Consider a deceptively simple Prolog program: p :- not q. q :- not p. Ask a classical logician what follows, and you'll get a shrug—the program is consistent but underdetermined. Ask three different logic programming systems, and you may receive three different answers: no models, two models, or a third truth value altogether. The same syntactic object encodes different computational meanings depending on which semantics interprets it.

This divergence is not a bug in logic programming; it is the field's central intellectual drama. When Kowalski proposed that algorithm = logic + control, he assumed the logical side was fixed. It wasn't. The introduction of negation-as-failure forced logic programming to abandon classical monotonicity, and once that boundary was crossed, multiple coherent formalizations became possible—each capturing different intuitions about what a rule set means.

For anyone building knowledge representation systems, answer set solvers, or hybrid neuro-symbolic architectures, the choice of semantics is not academic. It determines termination behavior, complexity class, and whether your system commits to bold conclusions or hedges cautiously. This article compares completion, stable model, and well-founded semantics, showing how each resolves the ambiguity of negation in structurally different ways—and why understanding those differences is essential for anyone deploying declarative reasoning at scale.

Classical logic treats negation as truth-functional: ¬p holds precisely when p is false in the model. Logic programming, driven by the pragmatics of finite databases and Horn-clause resolution, adopted a radically different rule. Under negation as failure (NAF), not p succeeds whenever the proof procedure fails to derive p in finite time. This is a meta-level operation on the derivation process, not a truth-functional operator on propositions.

The consequence is non-monotonicity. In classical logic, adding axioms can only expand the set of theorems. Under NAF, adding the fact p. to a program can invalidate previously derived conclusions that depended on not p. This mirrors how humans reason from incomplete information—we conclude birds fly, then retract when told about penguins—but it breaks the tidy compositional guarantees classical proof theory provides.

The closed-world assumption (CWA) underwrites this move. If our knowledge base is presumed complete for the predicates it defines, absence of evidence becomes evidence of absence. This is defensible for a flight schedule database, questionable for a medical diagnostic system, and philosophically fraught for open-domain reasoning. Every semantics we examine represents a different formalization of what CWA should mean when programs contain recursion through negation.

SLDNF resolution, the operational backbone of Prolog, implements NAF procedurally: to evaluate not p, launch a subproof of p, and if it finitely fails, succeed. But this leaves floundering queries and infinite loops as unresolved corner cases. The declarative question—what does the program mean, independent of any particular procedure?—demanded a model-theoretic account.

That demand produced not one answer but a family, because negation through recursion genuinely admits multiple defensible interpretations. The program p :- not p. has no classical model, but should it be inconsistent, three-valued, or simply reject the query? Each semantics we now examine gives a principled, but different, reply.

Takeaway

Negation-as-failure trades classical monotonicity for pragmatic completeness assumptions—a bargain that produces multiple coherent semantics, not one canonical meaning.

Keith Clark's 1978 program completion was the first serious attempt to give NAF a declarative reading in classical logic. The idea is elegant: interpret the programmer's rules as only-if definitions in addition to their surface if reading. If the program contains p :- q. and p :- r., the completion produces p ↔ q ∨ r. Predicates with no defining clauses are equivalenced with false.

This transformation converts a logic program into a classical first-order theory (with an equality theory for term structure), and NAF becomes classical negation over that completed theory. When the completion is consistent and categorical, it captures programmer intent beautifully: definitions are treated as biconditional, matching the way most programmers actually think when they write rules.

The trouble arises with recursion through negation. Consider p :- not p. Its completion is p ↔ ¬p, a classical contradiction. Yet operationally, this program is not incoherent—it simply loops. Completion declares inconsistency where a more refined semantics would identify the atom as undefined. Similarly, the even/odd program defining natural number parity via mutual recursion has a completion with unintended non-standard models.

Fitting's three-valued completion repaired much of this by moving to Kleene's strong three-valued logic, where p ↔ ¬p is satisfiable with p assigned the third value. This foreshadowed the well-founded semantics and revealed that completion's real limitation was its commitment to two-valued classical logic, not the biconditional idea itself.

Completion remains the semantics of choice when programs are stratified—when negation never occurs within a recursive cycle. For such programs, completion, stable, and well-founded semantics all coincide, and completion offers the most direct bridge to SAT solvers and classical theorem provers. Modern ASP grounders exploit this by translating stratified fragments directly to propositional formulas.

Takeaway

Completion works by making implicit definitions explicit—but only stratified programs escape the pathologies that recursive negation introduces into the biconditional reading.

The 1988-1991 period produced the two dominant semantics for unrestricted logic programs. Stable model semantics, due to Gelfond and Lifschitz, defines a model M as stable if it equals the least Herbrand model of the reduct—the program obtained by (i) deleting rules whose negative body is falsified by M, and (ii) removing the remaining negative literals. This fixpoint condition captures a rational agent's self-supporting belief state.

Stable semantics is credulous in flavor: a program may have zero, one, or many stable models, and each represents a distinct coherent way of resolving the program's negative loops. The program p :- not q. q :- not p. has two stable models—{p} and {q}—each internally consistent. This multiplicity is precisely what answer set programming exploits: enumerate stable models to enumerate solutions to combinatorial problems.

The well-founded semantics of Van Gelder, Ross, and Schlipf takes the opposite stance. It computes a unique three-valued model by alternating fixpoint iteration of an operator that identifies atoms as true, false, or undefined. For the two-loop program above, well-founded semantics assigns both p and q the value undefined—refusing to commit where the program is genuinely ambivalent.

The computational profiles diverge sharply. Deciding whether an atom is in some stable model is Σ₂ᵖ-complete for propositional programs; deciding well-founded truth is polynomial. Well-founded semantics is the natural fit for query-driven database systems (SLG resolution, XSB Prolog), where tractability and definiteness matter. Stable semantics is the natural fit for search and configuration problems (clingo, DLV), where enumerating alternatives is the point.

Crucially, the two are not competitors but complements: the well-founded model is always contained in the intersection of all stable models. Modern ASP solvers use well-founded computation as a propagation engine inside stable model search, extracting the polynomial-time skeptical consequences before branching on the remaining undefined atoms.

Takeaway

Skeptical semantics preserves tractability by refusing to guess; credulous semantics accepts complexity in exchange for enumerating every coherent resolution. Choose your tradeoff deliberately.

The plurality of logic programming semantics is not a failure to converge on truth—it is a recognition that negation through recursion is genuinely ambiguous, and different applications demand different resolutions. Completion serves stratified deduction; well-founded serves tractable query answering; stable serves combinatorial search. Each is optimal for its niche and pathological outside it.

For practitioners, the lesson is architectural: match the semantics to the reasoning task before selecting the solver. Deploying an ASP system where well-founded suffices is expensive; deploying Prolog where stable model enumeration is needed is incorrect. The semantics is a design decision, not an implementation detail.

As neuro-symbolic systems increasingly embed declarative reasoning within learned components, this design space becomes more relevant, not less. The question what does this rule set mean? admits no single answer—and understanding the alternatives is what separates competent knowledge engineers from those who merely wield the tools.