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.

Metatheory. Every normal program has a unique well-founded (three-valued) model, computed as the least fixpoint of the monotone operator W_P; it always exists and is polynomial-time computable for propositional programs (contrast: deciding answer-set existence is NP-complete). It coincides with the stable model when total, and soundly approximates the intersection of all stable models otherwise. It agrees with the perfect model on stratified programs and extends smoothly to well-founded semantics for extended and disjunctive fragments.

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/three-valued: it leaves genuinely contested atoms undefined rather than exploring alternatives, so it cannot express problems whose solutions are the multiple stable models (e.g., combinatorial search). Weaker than answer-set semantics for knowledge representation. Handling disjunction and strong negation requires further, less canonical extensions.

© 2026 Lingenic LLC