Skip to content

Semantics: open vs closed world, NAF, WFS, and ASP

One innocent-looking symbol — negation — hides some of the deepest design choices in logic programming. When you write "not Flies(tweety)", what does it mean?

  • Is it false, or merely not known to be true?
  • If you learn a new fact tomorrow, can a conclusion you drew today be withdrawn?
  • If two conclusions are locked in a mutual "each is true unless the other is", is the answer two possible worlds, no world at all, or "undefined"?

Different logics answer these questions differently. This notebook is an executable tour of those answers. Every claim below is backed by a solver you can re-run — no hand-waving.

We author each theory in TLog, the compact text syntax for typedlogic, so the logic reads directly instead of hiding inside Python strings. The same theory files are loaded and handed to different solvers.

We cover four ideas and the relationships between them:

Idea One-line intuition Illustrated with
Open-World Assumption (OWA) absence of a fact means unknown Z3 (classical FOL)
Closed-World Assumption (CWA) absence of a fact means false Clingo, Datalog
Negation as Failure (NAF) not p succeeds if p can't be proven Clingo
Answer Set Programming (ASP) stable models: enumerate self-consistent worlds Clingo
Well-Founded Semantics (WFS) three-valued: true / false / undefined WellFoundedSolver

These correspond directly to profile classes shipped in typedlogic.profiles (OpenWorld, ClosedWorld, WellFoundedSemantics, ClassicPrologNegationAsFailure, AnswerSetProgramming), which we revisit at the end.

Setup

This notebook uses the Z3, Clingo, and ProbLog integrations:

pip install 'typedlogic[z3,clingo,problog]'

Z3 is a classical first-order theorem prover — it embodies the open-world, monotonic view. Clingo is an Answer Set Programming solver — the closed-world, non-monotonic view. Putting them side by side is the whole point; WellFoundedSolver (built in) adds the three-valued middle ground.

Each theory lives in a .tlog file next to this notebook. Two tiny helpers let us show a theory (with syntax highlighting) and load it for a solver.

from pathlib import Path
from IPython.display import Code

from typedlogic import Term, Not
from typedlogic.parsers.tlog_parser import TLogParser
from typedlogic.integrations.solvers.z3 import Z3Solver
from typedlogic.integrations.solvers.clingo import ClingoSolver
from typedlogic.integrations.solvers.wellfounded import WellFoundedSolver, NegativeCycleError

HERE = Path("semantics")  # the .tlog theory files live here

def show(name):
    "Display a .tlog theory with syntax highlighting."
    return Code(filename=str(HERE / name), language="prolog")

def load(name):
    "Parse a .tlog theory file into a Theory."
    return TLogParser().parse((HERE / name).read_text())

1. Open world vs closed world

Consider a tiny flight database. There is a direct flight SFO→JFK and JFK→LHR. There is no row for SFO→LHR.

show('flights.tlog')

pred DirectFlight(src: str, dst: str).

DirectFlight("sfo", "jfk").
DirectFlight("jfk", "lhr").

The question: Is there a direct flight from SFO to LHR? We never asserted one. What should a reasoner say?

Closed world (Clingo)

A closed-world reasoner treats the database as complete. Anything not derivable is taken to be false. Clingo returns exactly one model — the facts we gave it — and DirectFlight(sfo, lhr) is simply absent, i.e. false.

solver = ClingoSolver()
solver.add(load("flights.tlog"))

model = list(solver.models())[0]
present = {t.values for t in model.iter_retrieve("DirectFlight")}
print("Direct flights in the (single) closed-world model:")
for t in sorted(present):
    print("  ", t)
print()
print("Is DirectFlight(sfo, lhr) in the model?", ("sfo", "lhr") in present)
print("=> Under CWA, 'no row' means FALSE.")

Direct flights in the (single) closed-world model:
   ('jfk', 'lhr')
   ('sfo', 'jfk')

Is DirectFlight(sfo, lhr) in the model? False
=> Under CWA, 'no row' means FALSE.

Open world (Z3)

A classical, open-world reasoner treats the database as partial. The absence of SFO→LHR tells us nothing. We can prove this operationally: a fact is entailed only if its negation is inconsistent with the knowledge base. So we check satisfiability both ways.

flights = load("flights.tlog")

# KB + DirectFlight(sfo,lhr): is it consistent?
s = Z3Solver(); s.add(flights); s.add(Term("DirectFlight", "sfo", "lhr"))
with_flight = s.check().satisfiable

# KB + NOT DirectFlight(sfo,lhr): is it consistent?
s = Z3Solver(); s.add(flights); s.add(Not(Term("DirectFlight", "sfo", "lhr")))
without_flight = s.check().satisfiable

print("KB +  DirectFlight(sfo,lhr) is satisfiable:", with_flight)
print("KB + ~DirectFlight(sfo,lhr) is satisfiable:", without_flight)
print()
print("Both are satisfiable => neither the flight nor its absence is entailed.")
print("=> Under OWA, 'no row' means UNKNOWN.")

KB +  DirectFlight(sfo,lhr) is satisfiable: True
KB + ~DirectFlight(sfo,lhr) is satisfiable: True

Both are satisfiable => neither the flight nor its absence is entailed.
=> Under OWA, 'no row' means UNKNOWN.

This is the fundamental split:

  • Closed world: what is not known to be true is false. Great for databases, configuration, policy checks — settings where you do have all the relevant facts.
  • Open world: what is not known to be true is unknown. Right for the semantic web, ontologies, and incomplete knowledge — where new facts can always arrive (this is the OWL/RDF world; see the OWL-DL tutorial).

Neither is "correct" in the abstract; they answer different questions. The bugs happen when you assume one and your tool implements the other.

2. Negation as failure, and non-monotonicity

The closed-world assumption gives us a cheap form of negation: not p succeeds precisely when we fail to prove p. This is negation as failure (NAF) — the negation of Prolog, Datalog, and ASP. In TLog, not is negation-as-failure, while ~ is classical/strong negation.

The classic use is default reasoning: birds fly, unless they are abnormal.

show('birds.tlog')

pred Bird(name: str).
pred Penguin(name: str).
pred Abnormal(name: str).
pred Flies(name: str).

Bird("tweety").
Bird("opus").
Penguin("opus").

/// Penguins are abnormal birds.
Abnormal(x) :- Penguin(x).

/// A bird flies UNLESS it can be shown abnormal.
/// `not` here is negation-as-failure.
Flies(x) :- Bird(x), not Abnormal(x).

Let's ask Clingo who flies.

def who_flies(extra_facts=()):
    s = ClingoSolver()
    s.add(load("birds.tlog"))
    for f in extra_facts:
        s.add(f)
    model = list(s.models())[0]
    return sorted(t.values[0] for t in model.iter_retrieve("Flies"))

print("Who flies by default?", who_flies())

Who flies by default? ['tweety']

tweety flies; opus does not (it's a penguin, hence abnormal). Nobody told us tweety is normal — the reasoner assumed it because it couldn't prove otherwise. That assumption is the closed world at work.

Now the crucial property. Watch what happens when we add a fact.

print("Before: ", who_flies())
print("Add Penguin(tweety) ...")
print("After:  ", who_flies(extra_facts=[Term("Penguin", "tweety")]))
print()
print("Learning MORE made us conclude LESS. This is NON-MONOTONICITY.")

Before:  ['tweety']
Add Penguin(tweety) ...
After:   []

Learning MORE made us conclude LESS. This is NON-MONOTONICITY.

Adding knowledge retracted a conclusion. Classical logic can never do this: it is monotonic — the set of entailed facts only ever grows. NAF buys expressiveness (defaults, exceptions, common-sense reasoning) at the price of monotonicity.

The same rule, read classically (Z3)

What if we read "birds fly unless abnormal" with classical negation (~) instead of NAF?

show('birds_classical.tlog')

pred Bird(name: str).
pred Abnormal(name: str).
pred Flies(name: str).

Bird("tweety").

/// The SAME rule, read with classical (strong) negation `~`
/// instead of negation-as-failure. Now `~Abnormal(x)` must be
/// *proven*, not merely assumed.
Flies(x) :- Bird(x), ~Abnormal(x).

Under the open world, we cannot conclude Flies(tweety) from Bird(tweety) alone — because ~Abnormal(tweety) is not entailed (it's merely unknown). We have to supply it.

bc = load("birds_classical.tlog")

# Is Flies(tweety) entailed from Bird(tweety) alone?
s = Z3Solver(); s.add(bc); s.add(Not(Term("Flies", "tweety")))
print("KB + ~Flies(tweety) satisfiable?", s.check().satisfiable,
      " => Flies(tweety) NOT entailed (abnormality is unknown, not false)")

# Now assert tweety is not abnormal, classically:
s = Z3Solver(); s.add(bc)
s.add(Not(Term("Abnormal", "tweety")))
s.add(Not(Term("Flies", "tweety")))
print("KB + ~Abnormal(tweety) + ~Flies(tweety) satisfiable?", s.check().satisfiable,
      " => now Flies(tweety) IS entailed")

KB + ~Flies(tweety) satisfiable? True  => Flies(tweety) NOT entailed (abnormality is unknown, not false)
KB + ~Abnormal(tweety) + ~Flies(tweety) satisfiable? False  => now Flies(tweety) IS entailed

So the very same English sentence means different things depending on the negation you pick:

  • NAF (not Abnormal): "assume normal unless proven abnormal" → concludes Flies(tweety) immediately, but retracts it later. Non-monotonic.
  • Classical (~Abnormal): "flies only if provably not abnormal" → stays agnostic until you supply the missing premise. Monotonic.

Choosing the wrong one is a real and common modelling bug.

3. When NAF loops: stable models (ASP)

Default reasoning was stratified — negation never depended on itself. Once we allow negation to loop back on itself, "what does not p mean" stops having an obvious answer, and the different semantics genuinely diverge. This is where ASP and WFS part ways.

Answer Set Programming answers with stable models (answer sets): each is a self-consistent world — a set of atoms that reproduces exactly itself when you apply the rules under its own negative assumptions. There can be several, or none.

Even loop → two worlds

show('even_loop.tlog')

pred p().
pred q().

/// p holds unless q does, and q holds unless p does.
p() :- not q().
q() :- not p().

"p holds unless q does, and q holds unless p does." Two coherent stories: p and not q, or q and not p.

solver = ClingoSolver()
solver.add(load("even_loop.tlog"))
models = list(solver.models())
print("Number of stable models (answer sets):", len(models))
for i, m in enumerate(models):
    print(f"  model {i}:", sorted(str(t) for t in m.ground_terms))

Number of stable models (answer sets): 2
  model 0: ['q']
  model 1: ['p']

Odd loop → no world

show('odd_loop.tlog')

pred p().

/// p holds if p does not: a paradoxical negative self-loop.
p() :- not p().

"p holds if p does not." No set of atoms can reproduce itself: assume p false and the rule forces it true; assume it true and the rule no longer fires. Zero stable models — the program is inconsistent in ASP.

solver = ClingoSolver()
solver.add(load("odd_loop.tlog"))
print("Satisfiable?", solver.check().satisfiable)
print("Number of stable models:", len(list(solver.models())))
print("=> An odd negative loop has NO answer set.")

Satisfiable? False
Number of stable models: 0
=> An odd negative loop has NO answer set.

Stable-model semantics is decisive and credulous: it hands you every self-consistent world, or refuses when none exists. That's ideal for combinatorial search (planning, configuration, graph coloring), but the "all or nothing" reaction to a loop can be surprisingly brittle.

4. A gentler answer: well-founded semantics

Well-founded semantics (WFS) refuses to guess. Instead of enumerating worlds it computes a single three-valued model: every atom is true, false, or undefined. Paradoxical loops land in undefined rather than exploding into many models or none.

typedlogic ships a WellFoundedSolver for exactly this. Its default native backend computes the well-founded model directly (via the standard Van Gelder alternating fixpoint) and reports the three-valued result. Run it on the same loops that gave ASP two models / zero models:

def well_founded(name):
    solver = WellFoundedSolver()            # backend="native" by default
    solver.add(load(name))
    m = solver.model()
    true = sorted(str(t) for t in m.ground_terms)
    undefined = sorted(str(t) for t in m.undefined_terms)
    return true, undefined

for name in ["even_loop.tlog", "odd_loop.tlog"]:
    true, undefined = well_founded(name)
    print(f"{name:16} TRUE={true}  UNDEFINED={undefined}")

even_loop.tlog   TRUE=[]  UNDEFINED=['p', 'q']


odd_loop.tlog    TRUE=[]  UNDEFINED=['p']

Compare the two semantics on the identical programs:

Program ASP (stable models) WFS (well-founded model)
p:-not q. q:-not p. two models: {p} and {q} one model: p, q both undefined
p:-not p. no model (inconsistent) one model: p undefined

ASP is credulous and brave: it commits to concrete worlds and enumerates them. WFS is skeptical and cautious: where the program is genuinely ambiguous or paradoxical, it declines to decide and marks the atom undefined — always yielding exactly one model, computable in polynomial time.

"Should we just wrap an existing engine?"

A fair question — WFS is well studied and has mature engines. The honest answer is it depends on the fragment, and the WellFoundedSolver backends make the trade-off concrete:

  • The problog backend delegates to ProbLog, a mature, wrapped engine. But ProbLog implements only the two-valued restriction of WFS: it agrees with the native backend on stratified programs, and refuses genuinely three-valued programs with a NegativeCycle error rather than reporting undefined.
  • The xsb backend is meant to drive XSB Prolog — the reference SLG/tabling engine — for large or deeply-recursive programs (requires the external xsb binary). It is experimental and not yet validated against a live XSB, so prefer native for now.
  • The native backend has no dependencies and returns the full three-valued model; it is the right tool for teaching and modestly-sized programs (grounding is naive, so it is not meant to compete with XSB on scale).

Watch ProbLog agree on the stratified default program, then refuse the negative loop:

# On a stratified program, the wrapped ProbLog engine and the native engine agree exactly.
native = WellFoundedSolver(backend="native"); native.add(load("birds.tlog"))
problog = WellFoundedSolver(backend="problog"); problog.add(load("birds.tlog"))
native_flies = sorted(str(t) for t in native.model().iter_retrieve("Flies"))
problog_flies = sorted(str(t) for t in problog.model().iter_retrieve("Flies"))
print("native  Flies:", native_flies)
print("problog Flies:", problog_flies)
print("agree?", native_flies == problog_flies)
print()

# On the even loop, ProbLog refuses rather than reporting 'undefined'.
try:
    s = WellFoundedSolver(backend="problog"); s.add(load("even_loop.tlog"))
    s.model()
except NegativeCycleError as e:
    print("problog on even_loop -> NegativeCycleError:")
    print(" ", str(e).split(".")[0] + ".")

native  Flies: ['Flies(tweety)']
problog Flies: ['Flies(tweety)']
agree? True

problog on even_loop -> NegativeCycleError:
  The 'problog' backend only supports programs with a total (two-valued) well-founded model; this program is genuinely three-valued.

That is the whole reason the native three-valued backend exists: no pip-installable engine returns undefined for these programs. WFS and the other semantics agree whenever the program is well-behaved (stratified) — here is the tweety/opus default program under all three, for confirmation:

# clingo (ASP), WFS native, WFS via problog -- all agree on the stratified program.
clingo = ClingoSolver(); clingo.add(load("birds.tlog"))
asp_flies = sorted(t.values[0] for t in list(clingo.models())[0].iter_retrieve("Flies"))

print("ASP (clingo)        Flies:", asp_flies)
print("WFS (native)        Flies:", native_flies)
print("WFS (problog)       Flies:", problog_flies)
print()
print("All agree: on stratified programs WFS, ASP and Datalog coincide.")

ASP (clingo)        Flies: ['tweety']
WFS (native)        Flies: ['Flies(tweety)']
WFS (problog)       Flies: ['Flies(tweety)']

All agree: on stratified programs WFS, ASP and Datalog coincide.

Putting it together: the typedlogic profiles

typedlogic reifies these semantic choices as profile classes in typedlogic.profiles, so a theory or solver can declare which assumptions it makes. The hierarchy encodes the relationships we just demonstrated — e.g. WellFoundedSemantics and ClassicPrologNegationAsFailure are both kinds of ClosedWorld, and AnswerSetProgramming is a WellFoundedSemantics that also permits MultipleModelSemantics (the several answer sets we saw). Each solver advertises its profile:

from typedlogic.profiles import (
    OpenWorld, ClosedWorld, SingleModelSemantics, MultipleModelSemantics,
)

solvers = [
    ("Z3 (classical FOL)",   Z3Solver()),
    ("Clingo (ASP)",         ClingoSolver()),
    ("WellFoundedSolver",    WellFoundedSolver()),
]

hdr = f"{'solver':22} {'closed?':8} {'open?':6} {'single?':8} {'multi?':7}"
print(hdr); print("-" * len(hdr))
for label, s in solvers:
    p = s.profile
    print(f"{label:22} {str(p.impl(ClosedWorld)):8} {str(p.impl(OpenWorld)):6} "
          f"{str(p.impl(SingleModelSemantics)):8} {str(p.impl(MultipleModelSemantics)):7}")

solver                 closed?  open?  single?  multi? 
-------------------------------------------------------
Z3 (classical FOL)     False    True   False    True   
Clingo (ASP)           True     False  False    True   
WellFoundedSolver      True     False  True     False

Takeaways

  • Open vs closed world decides what silence means: unknown, or false. Pick by whether your data is complete.
  • Negation as failure gives cheap, powerful default reasoning — and with it non-monotonicity: new facts can retract old conclusions. Classical negation stays monotonic but can't express defaults.
  • When negation loops, ASP enumerates stable worlds (two, or none), while WFS computes a single three-valued model that marks the ambiguity undefined. They coincide on stratified programs.
  • The WellFoundedSolver gives you WFS directly, with a native three-valued engine, a wrapped ProbLog backend for the two-valued fragment, and an (experimental) XSB backend for scale.
  • typedlogic.profiles lets you name the assumption you rely on, so a mismatch between what you meant and what your solver does becomes explicit rather than a silent bug.

Where to go next

  • Multiple models — the multiple-models notebook explores enumerating worlds with Clingo in more depth.
  • Open-world modelling — the OWL-DL tutorial is the open-world assumption applied to ontologies.
  • TLog syntax — the TLog parser docs document the text syntax used for the theories here.