The concept of a stable model, or answer set, is used to define a declarative semantics for logic programs with negation as failure.
Research on the declarative semantics of negation in logic programming was motivated by the fact that the behavior of SLDNF resolution—the generalization of SLD resolution used by Prolog in the presence of negation in the bodies of rules—does not fully match the truth tables familiar from classical propositional logic.
The discovery of these relationships was a key step towards the invention of the stable model semantics.
The syntax of autoepistemic logic uses a modal operator that allows us to distinguish between what is true and what is known.
The stable model semantics, in its basic form, can be viewed as a reformulation of this idea that avoids explicit references to autoepistemic logic.
Nicole Bidoit and Christine Froidevaux [1987] proposed to treat negated atoms in the bodies of rules as justifications.
The stable model semantics uses the same idea, but it does not explicitly refer to default logic.
This convention allows us to use the set inclusion relation to compare truth assignments with each other.
To extend this definition to the case of programs with negation, we need the auxiliary concept of the reduct, defined as follows.
(Indeed, this set of atoms satisfies every rule of the reduct, and it has no proper subsets with the same property.)
If we think of the stable model semantics as a description of the behavior of Prolog in the presence of negation then programs without a unique stable model can be judged unsatisfactory: they do not provide an unambiguous specification for Prolog-style query answering.
In this section, as in the definition of a stable model above, by a logic program we mean a set of rules of the form where
Fangzhen Lin and Yuting Zhao [2004] showed how to make the completion of a nontight program stronger so that all its nonstable models will be eliminated.
The well-founded model of a logic program partitions all ground atoms into three sets: true, false and unknown.
In the context of logic programming, this idea leads to the need to distinguish between two kinds of negation—negation as failure, discussed above, and strong negation, which is denoted here by
A school bus may cross railway tracks under the condition that there is no approaching train.
The weaker rule, that uses strong negation in the body, is preferable: It says that it's okay to cross if we know that no train is approaching.
To incorporate strong negation in the theory of stable models, Gelfond and Lifschitz [1991] allowed each of the expressions
An alternative approach [Ferraris and Lifschitz, 2005] treats strong negation as a part of an atom, and it does not require any changes in the definition of a stable model.
Coherent stable models of a program are identical to its consistent answer sets in the sense of [Gelfond and Lifschitz, 1991].
The stable model semantics has been generalized to many kinds of logic programs other than collections of "traditional" rules discussed above—rules of the form where
One simple extension allows programs to contain constraints—rules with the empty head: Recall that a traditional rule can be viewed as alternative notation for a propositional formula if we identify the comma with conjunction
The properties of the stable model semantics stated above for traditional programs hold in the presence of constraints as well.
To extend the stable model semantics to disjunctive programs [Gelfond and Lifschitz, 1991], we first define that in the absence of negation (
As in the traditional case, the stable models of a disjunctive program are minimal and form an antichain.
David Pearce [1997] and Paolo Ferraris [2005] showed how to extend the definition of a stable model to sets of arbitrary propositional formulas.
Instead of reducts, it refers to equilibrium logic—a system of nonmonotonic logic based on Kripke models.
The two approaches to defining stable models for sets of propositional formulas are equivalent to each other.
is also a stable model of the same formula, written in logic programming notation, in the sense of the original definition.
The minimality and the antichain property of stable models of a traditional program do not hold in the general case.