TLDR
- Negation is evaluated against a candidate. Assume a set M of true ground atoms, then use M to decide which negative body literals succeed.
- The reduct removes negation. Delete any rule defeated by M; from every surviving rule delete all negative literals.
- A stable model is self-reproducing. M is stable exactly when it equals the unique minimal Herbrand model of its positive reduct.
- Programs need not be stratified. The construction handles useful negative cycles beyond iterated fixed-point semantics, though not every program has one canonical answer.
- The 1988 scope is narrower than modern ASP. The paper calls the semantics defined only when there is exactly one stable model; later practice treats multiple stable models as answer sets.
A programme can have too many ordinary models
A logic-program rule can be read as a first-order formula. That grants it ordinary models, but ordinary truth alone usually does not determine the intended answers to database or Prolog queries.
The paper considers rules of the form A ← L₁,…,Lₘ, where the head A is an atom and each body item is an atom or a negated atom. Read declaratively, the conjunction of the body implies the head. A set of such formulas typically has many models because truth may contain unsupported extras. The semantic task is to choose a canonical model: the atoms that count as correct consequences of the programme.
For the positive programme p(1), q(2), and q(x) ← p(x), both {p(1),q(1),q(2)} and the larger set that additionally contains p(2) are Herbrand models. The extra p(2) is not forced by a fact or rule. The usual semantics for negation-free programmes selects the unique minimal Herbrand model, excluding gratuitous atoms.
A Herbrand universe is built from the ground terms of the programme; constants and functions denote themselves. A Herbrand interpretation can be identified with the set of ground atoms it makes true. This syntactic anchoring turns model selection into a set problem. A model M is minimal when no proper subset is also a model: not necessarily minimum in cardinality, and not necessarily unique once negation enters.
Negation as failure creates the difficulty. A negative body literal says that an atom lacks support, so whether a rule fires depends on what the completed interpretation contains. Stratified programmes order predicates into layers and evaluate lower layers before negative uses at higher ones. But useful programmes can contain cycles through negation that no such ordering permits.
Worked example 1 · remove the unsupported atom
In the positive programme above, adding p(2) forces nothing new beyond q(2), which was already a fact. Deleting p(2) leaves every rule true. The larger interpretation is therefore not minimal; the smaller one is the canonical model.
Causal probe 1 · why not accept every classical model?
A query for p(2) would receive both yes and no across permitted models even though the programme supplies no derivation. Minimality makes truth earn its place through facts and rules rather than arbitrary enlargement.
First make every rule concrete
The stable-model definition operates on ground atoms. Variables are replaced by all ground instances before a candidate is tested, even when function symbols make the resulting programme infinite.
Grounding is not an optional implementation trick in the 1988 definition. It supplies the universe over which M ranges and makes each negative literal a direct membership question: is B in M? For a finite function-free programme, one can enumerate every substitution of constants. With function symbols, the Herbrand universe and ground programme may be infinite, but the mathematical transformation is still defined.
Once negation is absent, a definite programme has a unique least: and therefore unique minimal: Herbrand model. It can be constructed by starting with no atoms, adding facts, then repeatedly adding any head whose positive body is already present. The process reaches a fixed point. This positive engine is familiar from van Emden and Kowalski; the innovation is to use a candidate interpretation to reduce a negative programme to this tractable form.
The distinction between “minimal” and “least” matters. A least model is contained in every model and is unique. A programme with negation may have incomparable minimal models. The reduct avoids ambiguity for each fixed candidate because it is positive and its least model is well determined. Ambiguity returns only at the outer level, where more than one candidate may reproduce itself.
Worked example 2 · grounding one variable
From q(x) ← p(x,y), not q(y) over constants 1 and 2, grounding produces four rules: q(1) for pairs (1,1) and (1,2), and q(2) for pairs (2,1) and (2,2). Candidate membership can now decide each not q(1) or not q(2) separately.
Causal probe 2 · why ground before taking the reduct?
A variable-level phrase such as not q(y) does not name one proposition whose truth M can settle. Grounding exposes every concrete negative dependency, allowing deletion to be a precise rule-by-rule operation.
Assume M, simplify by M, derive M
The Gelfond–Lifschitz reduct separates two roles of negation: the candidate decides negative premises; positive consequence then checks whether the candidate’s affirmative atoms are justified.
Given a ground programme Π and any set M of its atoms, form Πᴹ in two steps. First delete every rule whose body contains not B with B in M. Such a negative premise is false under the candidate, so the rule cannot support its head. Second, delete every negative literal from every rule that survives. For those literals B is absent from M, so their negative conditions have already succeeded.
The reduct is positive. Let SΠ(M) denote its minimal Herbrand model. A stable set is a fixed point: SΠ(M)=M. The paper then calls stable sets stable models, because Theorem 1 proves that every stable set is a minimal Herbrand model of the original programme. The converse does not hold: minimality alone does not ensure that a candidate is regenerated by its own reduct.
This is a foundedness test. Candidate atoms do not become true merely because M assumed them. After negation has been evaluated, each member must reappear through a fact or a positive chain in Πᴹ. Conversely, the reduct may derive an atom omitted by M; that candidate also fails. Stability demands exact equality, not mere modelhood or inclusion.
The authors connect the intuition to stable expansions in autoepistemic logic. If M is the set of atoms I believe, any rule containing not B with B in M is useless from my point of view; any not B with B absent is trivial. I simplify the premises accordingly. If precisely M follows from the simplified premises, the belief set is rational in their stated sense.
Worked example 3 · a successful candidate
For p ← not q and q ← not p, try M={p}. The q-rule is deleted because p∈M. The surviving p-rule loses not q and becomes the fact p. Its least model is {p}, so the assumption regenerates itself.
Causal probe 3 · why use two phases?
If negative and positive reasoning were interleaved without a candidate, a negative cycle could oscillate procedurally. Fixing M makes every negative test definite; the positive reduct then has one least-model result that can be compared back to M.
Exact reduct laboratory
Choose one of four ground programmes. The laboratory enumerates every candidate subset, constructs its reduct, computes the positive least model and marks exact fixed points.
Worked example 4 · two stable alternatives
For p ← not q and q ← not p, {p} reduces the programme to the fact p, while {q} reduces it to q. Both return themselves. ∅ reduces to two facts and returns {p,q}; {p,q} deletes both rules and returns ∅. Exactly two candidates are stable.
Causal probe 4 · what does enumeration expose?
Each candidate owns a different positive reduct. Showing every candidate prevents a common mistake: computing one minimal model of the original negative programme and calling it stable without checking self-reproduction.
A negative dependency need not destroy a unique meaning
Gelfond and Lifschitz’s principal example has a recursion through negation that stratification rejects, yet the reduct identifies one stable model.
Programme (5) contains the fact p(1,2) and the rule q(x) ← p(x,y), not q(y). Its four ground instances include q(1) ← p(1,2), not q(2). Try M={q(2)} and the reduct derives p(1,2) but not q(2), so the candidate fails even before noting that it was not a model of the original programme.
Now try M={p(1,2),q(1)}. Because q(1) is in M, rules requiring not q(1) are deleted. Because q(2) is absent, surviving rules with not q(2) lose the negative literal. The ground instance q(1) ← p(1,2) survives, so positive closure derives q(1) from the fact. The reduct’s least model is exactly M.
The authors narrow the remaining search. Every value of SΠ contains p(1,2), because it is a fact, and excludes p(1,1), p(2,1) and p(2,2), because no rule derives them. Only four candidate shapes remain, and direct examination finds no other fixed point. The programme therefore has a unique stable model despite lacking a stratification.
They note two uses. Prolog’s query evaluation handles this programme correctly relative to the stable model: a ground query receives yes exactly for members of the model. A related rule can describe winning positions in a loop-free two-player game: a position is winning when it has a legal move to a position not winning for the opponent. The loop-free proviso matters, as later examples show.
Worked example 5 · derive q(1)
Under M={p(1,2),q(1)}, q(2) is absent. The rule instance q(1) ← p(1,2), not q(2) survives and becomes q(1) ← p(1,2). The fact supplies its body, so q(1) earns support in the reduct.
Causal probe 5 · why can an unstratified programme still be stable?
Stratification is a sufficient syntactic schedule, not the definition of semantic coherence. A particular candidate can resolve the negative cycle so that the remaining positive dependencies uniquely justify it.
Not every programme chooses a canonical world
The fixed-point definition is simple enough to make failure modes visible. An odd loop through negation has no stable model; a symmetric even loop has two.
For p ← not p, candidate ∅ leaves the rule and erases its negative literal, producing the fact p; the least model is {p}. Candidate {p} deletes the rule, producing an empty programme whose least model is ∅. The operator swaps the two candidates rather than fixing either. No stable model exists.
For p ← not q and q ← not p, there are two fixed points, {p} and {q}. Each assumes one atom, defeats the other atom’s rule, and turns its own rule into a fact. The programme’s symmetry gives no reasonable basis for selecting one as the unique canonical model. The authors say the stable-model semantics is not applicable to programmes with none or several stable models.
That sentence marks a historical boundary. Modern answer-set programming commonly calls every stable model an answer set and deliberately uses multiplicity to represent alternatives; constraints and optimisation can then filter or rank them. The 1988 paper instead frames its goal as selecting one canonical model for query answering. Its formal fixed points enable the later practice, but the declared semantics is narrower.
Programme (6), p ← q, not r; q ← r, not p; r ← p, not q, offers another warning about dependency graphs. Its only minimal Herbrand model is ∅, and ∅ is stable because every rule body contains a positive atom; the reduct still has no initial fact, so closure remains empty. A negative cycle does not by itself force choice or inconsistency. Positive support structure determines what can start.
Worked example 6 · odd negation oscillates
The two possible candidates for p ← not p map to one another: SΠ(∅)={p}, while SΠ({p})=∅. The absence of a fixed point is not a search failure; it is the semantics’ diagnosis.
Worked example 7 · an empty stable model
In programme (6), candidate ∅ leaves every negative condition satisfied, but erasing those conditions yields p←q, q←r and r←p. With no facts, positive closure derives nothing. The empty candidate therefore regenerates itself.
Causal probe 6 · why doesn’t a cycle create its own support?
The least model of a positive cycle without a fact is empty. Circular permission is not a derivation seed. Stability preserves this groundedness after negative premises have been settled.
Agreement on the well-behaved fragment
A new semantics is more credible when it preserves established answers where established methods apply. The paper locates stable models relative to positive, well-founded, perfect and iterated fixed-point semantics.
If a programme contains no negation, every reduct is the programme itself, regardless of M. The positive least model is therefore the operator’s only fixed point and the only stable model. Stable semantics conservatively extends the ordinary least-Herbrand-model account.
Theorem 2, credited to the then-current well-founded work of Van Gelder, Ross and Schlipf, says that if Π has a well-founded model, that model is its unique stable model. Their examples show the stable semantics is strictly more general in the sense used there: some programmes with a unique stable model fall outside that well-founded account.
Because well-founded and perfect semantics coincide on locally stratified programmes, Corollary 1 gives a unique stable model identical to the perfect model for every locally stratified programme. Because perfect and iterated fixed-point semantics coincide on stratified programmes, Corollary 2 makes the analogous claim for ordinary stratification. Programme (5) shows that agreement does not define the boundary: stable models can reach beyond it.
The comparison is not a total ordering over arbitrary non-locally-stratified programmes. The paper notes partial overlap with perfect-model semantics: programme (5) is stable but not covered by perfect semantics, whereas the ordinary Herbrand model of p ← not p is perfect in the cited sense but not stable. “More general” is tied to the well-founded relation in Theorem 2, not a claim that stable semantics accepts every programme another proposal accepts.
Worked example 8 · stratified agreement
Take bird(x) ← penguin(x) and flies(x) ← bird(x), not abnormal(x), with abnormal decided in a lower stratum. Evaluating strata first or guessing the completed candidate and taking its reduct yields the same unique model.
Causal probe 7 · why prove coincidence results?
Without them, a semantics that handles exotic cycles might silently change ordinary database answers. Coincidence shows that the new fixed point preserves the established core while enlarging the usable class.
Negation as absence of grounds for belief
The reduct is presented as a simpler implementation of an idea already expressed through autoepistemic logic: place a belief operator after programme negation.
For a ground logic programme Π, the translation I(Π) replaces each negative body literal not B by ¬LB, where L is the modal belief operator. The result says that a rule may use B’s failure when B is not believed. Stable expansions close a theory under its consequences together with positive introspection for included formulas and negative introspection for excluded formulas.
Theorem 3 addresses the unique case central to the paper: if Π has a unique stable model M, then I(Π) has a unique stable expansion E and M is exactly the set of programme atoms in E. The proof uses a lemma reducing expansions to the objective programme selected by their atom set, then observes that objective theories have a uniquely determined stable expansion.
The theorem does not make the reduct a syntactic abbreviation for every feature of autoepistemic logic. It establishes correspondence for the stated translation and unique-model condition. The authors’ point is methodological: one can realise the belief-set intuition without requiring a reader or implementation to manipulate modal logic during the basic definition.
This connection also locates stable models in the non-monotonic landscape developed earlier in the canon. Reiter’s defaults use consistency tests; Moore’s autoepistemic logic uses beliefs about belief; circumscription minimises designated predicates. Stable semantics combines a candidate-dependent interpretation of failure with minimal positive derivability. Similar aims do not make the mechanisms interchangeable.
Worked example 9 · translating a negative premise
The rule p ← not q becomes ¬Lq ⊃ p. In expansion corresponding to {p}, q is not believed, so the antecedent holds and p follows. In the competing expansion corresponding to {q}, q is believed and that rule supplies no p.
Causal probe 8 · what does the belief operator clarify?
It distinguishes classical ¬q from failure to believe q. Logic-program negation need not claim q is false in an independently given world; it tests the candidate’s epistemic closure.
From unique canonical models to answer sets
The eleven-page paper defines a transformation whose afterlife became larger than its original presentation. Fidelity requires separating the 1988 claims from the later answer-set programming paradigm.
The original article proposes a declarative semantics for normal logic programmes with negation, proves stable models minimal, gives non-stratified examples, records non-existence and multiplicity, and connects unique stable models to well-founded, perfect, stratified and autoepistemic accounts. It does not present a solver, complexity analysis, grounding optimisation, disjunctive heads, classical negation, constraints, aggregates or optimisation statements.
Later work retained the reduct while changing how multiplicity is used. Stable models became answer sets: several models can encode alternatives, and the computational task is to find one or all of them. The 1991 extension by Gelfond and Lifschitz added classical negation and disjunctive databases; subsequent systems developed efficient grounding and solving. Marek and Truszczyński’s 1999 account explicitly presents stable models as an alternative programming paradigm.
The transformation also became a reference point for extensions: nested expressions, aggregates, constraint atoms, first-order and higher-order generalisations: and for alternative characterisations using completions, loop formulas or fixpoint theory. These developments should not be retrojected into the primary paper. What belongs to 1988 is the simple candidate/reduct/least-model fixed point and its initial comparison theorems.
The evidence is theoretical. The paper’s programme examples are exact witnesses, not performance experiments. Its Prolog remark concerns correctness for one example, not equivalence with every operational behaviour. Its game remark assumes a loop-free graph; adding a loop can make the representation meaningless in the authors’ own account. The stable-model idea is powerful partly because it makes such boundaries mathematically inspectable.
Evidence boundary
“Foundation of answer-set programming” is a later historical assessment. The primary paper itself seeks one canonical model and declares its semantics inapplicable when stable models are multiple. This companion names both facts so the later success does not overwrite the original scope.
Causal probe 9 · why did multiplicity become useful?
A symmetric pair of stable models is a problem if a database query requires one canonical truth set. It becomes a feature when a programme specifies a search problem and each model represents one admissible solution.
Minimality follows; existence does not
The paper’s short proofs support precise claims. They do not establish that every minimal model is stable, that every programme has a stable model, or that stability can always choose one model.
For Theorem 1, suppose M is stable. Each original rule is true in M: a rule deleted from the reduct has a negative literal not B falsified by B∈M, making the implication true; a surviving rule corresponds to a positive reduct rule satisfied by M. Now suppose a proper subset M₁ of M were also an original model. Every negative literal that survived under M also holds under M₁, because its atom was absent from M and therefore absent from the subset. M₁ would satisfy the reduct, contradicting that M is its minimal model.
The subset direction is crucial. It cannot prove uniqueness among incomparable stable models, and indeed the even negative cycle supplies two. Nor does original modelhood guarantee reduct modelhood for the same candidate, because negative assumptions determine which supports remain.
The operator SΠ is generally non-monotonic. Adding atoms to M can delete more rules from Πᴹ and therefore shrink the least model, as p ← not p demonstrates. Standard ascending fixed-point iteration over candidate sets is not licensed. The laboratory safely enumerates finite candidates; practical solvers use more sophisticated search and propagation developed later.
Worked example 10 · minimal but not stable is possible
Minimality checks only whether an original model has a smaller original model. Stability additionally checks whether the candidate’s treatment of negation leaves positive grounds for exactly its atoms. Theorem 1 runs in one direction for that reason.
Causal probe 10 · what fails in naïve iteration?
If M grows, more negative premises fail and more rules disappear; SΠ(M) may shrink. An operator that reverses direction can alternate instead of converging, so ordinary positive closure applies only inside each reduct.
| Statement | Status in the 1988 paper | Consequence |
|---|---|---|
| Every stable model is a minimal Herbrand model. | Theorem 1, proved. | Stable truth contains no removable unsupported enlargement. |
| Every minimal Herbrand model is stable. | Not proved and false in general. | Minimality is necessary, not sufficient. |
| Every programme has exactly one stable model. | Explicitly false; §3 gives zero and two. | The original canonical semantics is partial. |
| Stratified programmes agree with earlier semantics. | Corollaries 1–2. | The construction preserves accepted answers on those fragments. |
| The reduct is a practical 1988 solver. | Not claimed. | The definition specifies models; implementation engineering came later. |
Twelve retrieval hooks
Scholarly and publication gates
Review A · fidelity, teaching and evidence fairness
The companion was checked against all eleven pages of the author-hosted primary scan, including the rule form, Herbrand examples (2)–(4), the exact two-stage definition of Πᴹ, Theorem 1 and its proof, programmes (5) and (6), Remarks 1–5, Theorem 2, both corollaries, the autoepistemic translation and Theorem 3. It preserves the paper’s unusual historical scope: “stable model semantics” is declared defined only for a programme with exactly one stable model. Multiple stable models are described as a case where no reasonable single canonical choice exists, not yet as answer sets. Later terminology is labelled later. The game interpretation retains the source’s loop-free qualification. No algorithmic-performance, complexity or solver claim is attributed to the paper.
Teaching review passed. The exposition separates grounding, candidate evaluation, rule deletion, negative-literal erasure, positive least-model construction and equality, then reunites them in exact examples. Ten worked examples and ten causal probes distinguish modelhood, minimality, leastness and stability. The none/one/many outcomes are treated symmetrically. The executable laboratory enumerates every subset for four small programmes rather than preprinting expected answers.
Review B · language, accessibility, responsive layout and execution
The prose was reviewed for inflated historical claims, vague authority, formulaic summary language, anthropomorphic drift and modern terminology projected backwards. British English is consistent. Each of ten figures has a unique title, description, caption and source note; diagrams use labels and shapes in addition to colour. Animation is non-essential and stops under reduced-motion preferences. The document has a skip link, ordered heading structure, labelled controls, live status, keyboard-operable interaction and high-contrast result states.
Responsive review covers widths of 1440, 768 and 390 pixels. The hero, TLDR cards, prose columns, laboratory, memory studio and sequence navigation collapse without horizontal overflow; equations and the review table remain independently scrollable where needed. Executable review covers all candidate subsets for all four programmes. Three invariants must pass: every reduct is negation-free; its reported least model is closed under every surviving rule and contains no derivable omission; and every reported stable model satisfies the original programme and has no proper-subset original model. Static worked examples preserve the lesson without scripting.
From terminological inheritance to self-justifying programmes
Paper 0098 made inheritance monotonic: a KL-ONE concept accumulates necessary restrictions and a classifier discovers its position. Paper 0099 turns to a different fixed point. Here a candidate set decides which failures count, those decisions change the rules, and the remaining positive programme must justify the candidate exactly. The contrast separates taxonomic consequence from non-monotonic model selection.
Paper 0100 returns to John McCarthy’s “Programs with Common Sense” and the Advice Taker. That earlier vision asks how a programme might receive declarative common-sense knowledge and improve through statements rather than reprogramming. Stable models later supply one precise answer to part of that ambition: how rules involving absence can determine coherent belief sets.
Sources and audit trail
- Gelfond, M., & Lifschitz, V. (1988). “The Stable Model Semantics for Logic Programming.” In R. A. Kowalski & K. A. Bowen (eds.), Proceedings of the Fifth International Conference and Symposium on Logic Programming, 1070–1080. MIT Press. Author-hosted primary scan.
- van Emden, M. H., & Kowalski, R. A. (1976). “The Semantics of Predicate Logic as a Programming Language.” Journal of the ACM, 23(4), 733–742. Positive least-model foundation cited by the primary paper.
- Van Gelder, A., Ross, K. A., & Schlipf, J. S. (1988). “Unfounded Sets and Well-Founded Semantics for General Logic Programs.” PODS, 221–230. The source for Theorem 2 as cited in 1988; the mature journal account appeared later.
- Moore, R. C. (1985). “Semantical Considerations on Nonmonotonic Logic.” Artificial Intelligence, 25(1), 75–94. Stable-expansion background for the autoepistemic comparison.
- Gelfond, M., & Lifschitz, V. (1991). “Classical Negation in Logic Programs and Disjunctive Databases.” New Generation Computing, 9, 365–385. Later extension; not part of the 1988 language.
- Marek, V. W., & Truszczyński, M. (1999). “Stable Models and an Alternative Logic Programming Paradigm.” In The Logic Programming Paradigm. Later answer-set perspective used only for historical context.
What ships with Paper 0099
Title: When a belief must regenerate itself: Gelfond and Lifschitz’s stable models. Standfirst: A visual, executable reconstruction of grounding, candidate-dependent reduction, positive closure and fixed-point stability. Search terms: stable model semantics, Gelfond Lifschitz reduct, logic programming, negation as failure, answer set programming, Herbrand model, non-monotonic reasoning. Demonstration: an exact enumerator covering positive closure, two stable alternatives, odd self-negation and the paper’s empty three-rule cycle. Accessibility promise: ten titled and described SVG figures, reduced-motion support, labelled controls, keyboard operation and responsive layouts.