Well-Founded Semantics

Origin. Van Gelder, Ross, and Schlipf (1988, 1991). A three-valued, uniquely-defined semantics for normal logic programs with negation-as-failure, giving every program a single intended model and standing as the main alternative to the (multiple, two-valued) stable-model/answer-set semantics.

Models. Skeptical meaning of programs with negation. Where stable-model semantics may yield several models or none, the well-founded semantics assigns exactly one three-valued model: atoms are true, false, or undefined. Undefined captures genuine circularity through negation (e.g., p ← ¬p), avoiding arbitrary choices and guaranteeing a total, tractable meaning.

Formalism.

Programs: Normal logic program: rules a ← b₁,…,bₘ, ¬c₁,…,¬cₙ. Herbrand base atoms take values in {true, false, undefined}.

Unfounded sets: A set U of atoms is unfounded w.r.t. a partial interpretation I if every rule with head in U has a body false in I or a positive body atom in U (no external support). The greatest unfounded set U_P(I) exists and collects atoms that cannot be justified.

Well-founded operator: T_P(I): immediate consequences (heads of rules whose bodies hold in I). W_P(I) = T_P(I) ∪ ¬.U_P(I) (derive supported atoms true, greatest unfounded set false). The least fixed point of the monotone W_P is the well-founded model.

Alternating fixpoint (Van Gelder): Iterate the Gelfond–Lifschitz-style operator; the alternating least/greatest fixpoints converge to the true and (complement of) false atoms; the gap is undefined.

Relation to answer sets: The well-founded model is a subset (approximation) of every stable model: what is true/false in it is true/false in all answer sets. If the well-founded model is total (no undefined), it is the unique stable model.

Symbols.

Symbol	Unicode	Name	Meaning
¬	U+00AC	Negation	Negation as failure in a rule body
←	U+2190	Leftwards arrow / Rule	Head holds if body holds
∪	U+222A	Set union	Joins the true and false parts in W_P
I	—	Partial interpretation	Assigns true, false or undefined to each atom
U	—	Unfounded set	Atoms with no support outside themselves
T_P	—	Immediate-consequence operator	Heads of rules whose bodies hold in I
U_P(I)	—	Greatest unfounded set	The largest unfounded set relative to I
W_P	—	Well-founded operator	T_P together with the negated greatest unfounded set
lfp	—	Least fixed point	Where iteration of W_P settles
t	—	True	Two-valued positive verdict
f	—	False	Two-valued negative verdict
u	—	Undefined	Third value, for circularity through negation

Metatheory. Van Gelder, Ross and Schlipf (1991) proved that every normal program has exactly one well-founded partial model, obtained as the least fixpoint of the monotone operator W_P; existence and uniqueness are unconditional, which is precisely what separates the semantics from the stable-model semantics, under which a program may have many models or none. Van Gelder (1993) gave the equivalent alternating-fixpoint construction: the Gelfond–Lifschitz operator is anti-monotone, so its square is monotone, and the least and greatest fixpoints of that square bound the true atoms and the non-false atoms, the gap between them being the undefined ones. The model coincides with the unique stable model when it is total, agrees with Przymusinski's perfect model on stratified programs, and otherwise soundly under-approximates the intersection of all stable models. Complexity separates the two semantics sharply: for datalog with negation the well-founded semantics is P-complete in data complexity and EXPTIME-complete in program complexity, whereas deciding whether a propositional normal program has a stable model at all is NP-complete.

Applies to. Deductive databases and query evaluation (recursion with negation). Logic-programming systems (XSB, SLG resolution, tabling). Approximation and pre-processing for answer-set solvers. Nonmonotonic reasoning where a single skeptical model is wanted.

Limitations. Skeptical and three-valued: contested atoms are left undefined rather than resolved into alternatives, so problems whose solutions just are the several stable models — graph colouring, planning, any combinatorial search — cannot be posed at all. The approximation of the stable models is sound but strictly incomplete: for p ← ¬q, q ← ¬p, r ← p, r ← q the two stable models both contain r, yet the well-founded model leaves p, q and r all undefined, so a consequence of every answer set is missed. Undefinedness also conflates two different situations, a genuine circularity through negation and a mere failure of the operator to decide, and nothing in the model distinguishes them. Disjunctive heads and strong negation fall outside the definition; the extensions that cover them are several and mutually inequivalent, so there is no canonical well-founded semantics beyond normal programs.