Stable model semantics: Difference between revisions

Revision as of 08:07, 17 July 2023

Latest revision as of 15:19, 25 August 2025

(6 intermediate revisions by 5 users not shown)

Line 3:

==Motivation==

Research on the declarative semantics of negation in logic programming was motivated by the fact that the behavior of [[SLD resolution#SLDNF|SLDNF]] resolution — theresolution—the generalization of [[SLD resolution]] used by [[Prolog]] in the presence of negation in the bodies of rules — doesrules—does not fully match the [[truth tables]] familiar from classical [[propositional logic]]. Consider, for instance, the program

:<math>p\ </math>

:<math>r \leftarrow p,\ q</math>

:<math>s \leftarrow p,\ \operatorname{not} q.</math>

Given this program, the query {{mvar|p}} will succeed, because the program includes {{mvar|p}} as a fact; the query {{mvar|q}} will fail, because it does not occur in the head of any of the rules. The query {{mvar|r}} will fail also, because the only rule with {{mvar|r}} in the head contains the subgoal {{mvar|q}} in its body; as we have seen, that subgoal fails. Finally, the query {{mvar|s}} succeeds, because each of the subgoals {{mvar|p}}, <math>\operatorname{not} q</math> succeeds. (The latter succeeds because the corresponding positive goal {{mvar|q}} fails.) To sum up, the behavior of SLDNF resolution on the given program can be represented by the following truth assignment:

Line 45:

==Relation to nonmonotonic logic==

The meaning of negation in logic programs is closely related to two theories of [[Nonmonotonic logic|nonmonotonic reasoning]]&nbsp;— [[autoepistemic logic]] and [[default 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 believedknown. [[Michael Gelfond]] [1987] proposed to read <math>\operatorname{not} p</math> in the body of a rule as "<math>p</math> is not believedknown", and to understand a rule with negation as the corresponding formula of autoepistemic logic. The stable model semantics, in its basic form, can be viewed as a reformulation of this idea that avoids explicit references to autoepistemic logic.

In default logic, a default is similar to an [[inference rule]], except that it includes, besides its premises and conclusion, a list of formulas called justifications. A default can be used to derive its conclusion under the assumption that its justifications are consistent with what is currently believedknown. Nicole Bidoit and Christine Froidevaux [1987] proposed to treat negated atoms in the bodies of rules as justifications. For instance, the rule

:<math>s \leftarrow p,\ \operatorname{not} q</math>

can be understood as the default that allows us to derive <math>s</math> from <math>p</math> assuming that <math>\neg q</math> is consistent. The stable model semantics uses the same idea, but it does not explicitly refer to default logic.

Line 71:

|}

is identified with the set <math>\{p,s\}</math>. This convention allows us to use the [[set inclusion]] relation to compare truth assignments with each other. The smallest of all truth assignments <math>\emptyset</math> is the one that makes every atom false; the largest truth assignment makes every atom true.

Second, a logic program with variables is viewed as shorthand for the set of all [[Ground expression|ground]] instances of its rules, that is, for the result of substituting variable-free terms for variables in the rules of the program in all possible ways. For instance, the logic programming definition of even numbers

:<math>\operatorname{even}(0)\ </math>

:<math>\operatorname{even}(s(X))\leftarrow \operatorname{not} \operatorname{even}(X)</math>

Line 81:

is understood as the result of replacing {{mvar|X}} in this program by the ground terms

:<math>0,\ s(0),\ s(s(0)),\dots.</math>

in all possible ways. The result is the infinite ground program

:<math>\operatorname{even}(0)\ </math>

:<math>\operatorname{even}(s(0))\leftarrow \operatorname{not} \operatorname{even}(0)</math>

Line 99:

:<math>A \leftarrow B_{1},\dots,B_{m},\operatorname{not} C_{1},\dots,\operatorname{not} C_{n}</math>

where <math>A,B_{1},\dots,B_{m},C_{1},\dots,C_{n}</math> are ground atoms. If {{mvar|P}} does not contain negation (<math>n=0</math> in every rule of the program) then, by definition, the only stable model of {{mvar|P}} is its model that is minimal relative to set inclusion.<ref>This approach to the semantics of logic programs without negation is due to Maarten van Emden and [[Robert Kowalski]] — {{harvnb|van Emden|Kowalski|1976}}.</ref> (Any program without negation has exactly one minimal model.) To extend this definition to the case of programs with negation, we need the auxiliary concept of the reduct, defined as follows.

For any set {{mvar|I}} of ground atoms, the ''reduct'' of {{mvar|P}} relative to {{mvar|I}} is the set of rules without negation obtained from {{mvar|P}} by first dropping every rule such that at least one of the atoms {{tmath|C_i}} in its body

Line 113:

To illustrate these definitions, let us check that <math>\{p,s\}</math> is a stable model of the program

:<math>p\ </math>

:<math>r \leftarrow p,\ q</math>

:<math>s \leftarrow p,\ \operatorname{not} q.</math>

The reduct of this program relative to <math>\{p,s\}</math> is

:<math>p\ </math>

:<math>r \leftarrow p,\ q</math>

:<math>s \leftarrow p.</math>

(Indeed, since <math>q\not\in\{p,s\}</math>, the reduct is obtained from the program by dropping the part <math>\operatorname{not} q.\ </math>) The stable model of the reduct is <math>\{p,s\}</math>. (Indeed, this set of atoms satisfies every rule of the reduct, and it has no proper subsets with the same property.) Thus after computing the stable model of the reduct we arrived at the same set <math>\{p,s\}</math> that we started with. Consequently, that set is a stable model.

Checking in the same way the other 15 sets consisting of the atoms <math>p,\ q,\ r,\ s</math> shows that this program has no other stable models. For instance, the reduct of the program relative to <math>\{p,q,r\}</math> is

:<math>p\ </math>

:<math>r \leftarrow p,\ q.</math>

The stable model of the reduct is <math>\{p\}</math>, which is different from the set <math>\{p,q,r\}</math> that we started with.

Line 151:

has no stable models.

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. For instance, the two programs above are not reasonable as Prolog programs&nbsp;— SLDNFprograms—SLDNF resolution does not terminate on them.

But the use of stable models in [[answer set programming]] provides a different perspective on such programs. In that [[programming paradigm]], a given search problem is represented by a logic program so that the stable models of the program correspond to solutions. Then programs with many stable models correspond to problems with many solutions, and programs without stable models correspond to unsolvable problems. For instance, the [[eight queens puzzle]] has 92 solutions; to solve it using answer set programming, we encode it by a logic program with 92 stable models. From this point of view, logic programs with exactly one stable model are rather special in answer set programming, like polynomials with exactly one root in algebra.

==Properties of the stable model semantics==

Line 179:

:<math>p \leftarrow p</math>

is the [[tautology (logic)|tautology]] <math>p \leftrightarrow p</math>. The model <math>\emptyset</math> of this tautology is a stable model of <math>p \leftarrow p</math>, but its other model <math>\{p\}\ </math> is not. François Fages [1994] found a syntactic condition on logic programs that eliminates such counterexamples and guarantees the stability of every model of the program's completion. The programs that satisfy his condition are called ''tight''.

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 additional formulas that they add to the completion are called ''loop formulas''.

Line 205:

From the perspective of [[knowledge representation]], a set of ground atoms can be thought of as a description of a complete state of knowledge: the atoms that belong to the set are known to be true, and the atoms that do not belong to the set are known to be false. A possibly ''incomplete'' state of knowledge can be described using a consistent but possibly incomplete set of literals; if an atom <math>p</math> does not belong to the set and its negation does not belong to the set either then it is not known whether <math>p</math> is true or false.

In the context of logic programming, this idea leads to the need to distinguish between two kinds of negation&nbsp;— negation—''[[negation as failure]]'', discussed above, and ''strong negation'', which is denoted here by <math>\sim</math>.<ref>{{harvnb|Gelfond|Lifschitz|1991}} call the second negation ''classical'' and denote it by <math>\neg</math>.</ref> The following example, illustrating the difference between the two kinds of negation, belongs to [[John McCarthy (computer scientist)|John McCarthy]]. A school bus may cross railway tracks under the condition that there is no approaching train. If we do not necessarily know whether a train is approaching then the rule using negation as failure

:<math>\hbox{Cross} \leftarrow \hbox{not Train}</math>

Line 223:

to be either an atom or an atom prefixed with the strong negation symbol. Instead of stable models, this generalization uses ''answer sets'', which may include both atoms and atoms prefixed with strong negation.

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. In this theory of strong negation, we distinguish between atoms of two kinds, ''positive'' and ''negative'', and assume that each negative atom is an expression of the form <math>{\sim} A</math>, where <math>A\ </math> is a positive atom. A set of atoms is called ''coherent'' if it does not contain "complementary" pairs of atoms <math>\ A,{\sim} A</math>. Coherent stable models of a program are identical to its consistent answer sets in the sense of [Gelfond and Lifschitz, 1991].

For instance, the program

Line 231:

:<math>q \leftarrow \operatorname{not} p</math>

:<math>r\ </math>

:<math>{\sim} r\leftarrow \operatorname{not}p</math>

has two stable models, <math>\{p,r\}\ </math> and <math>\ \{q,r,{\sim} r\}</math>. The first model is coherent; the second is not, because it contains both the atom <math>\ r</math> and the atom <math>\ {\sim} r</math>.

===Closed world assumption===

According to [Gelfond and Lifschitz, 1991], the [[closed world assumption]] for a predicate <math>p\ </math> can be expressed by the rule

:<math>\sim p(X_1,\dots,X_n)\leftarrow\operatorname{not}p(X_1,\dots,X_n)</math>

(the relation <math>p\ </math> does not hold for a tuple <math>X_1,\dots,X_n</math> if there is no evidence that it does). For instance, the stable model of the program

:<math>p(a,b)\ </math>

:<math>p(c,d)\ </math>

:<math>\sim p(X,Y)\leftarrow\operatorname{not}p(X,Y)</math>

Line 253:

consists of 2 positive atoms

:<math>p(a,b),\ p(c,d)\ </math>

and 14 negative atoms

:<math>\sim p(a,a),\ {\sim} p(a,c),\ \dots</math>

i.e., the strong negations of all other positive ground atoms formed from <math>p,\ a,\ b,\ c,\ d</math>.

A logic program with strong negation can include the closed world assumption rules for some of its predicates and leave the other predicates in the realm of the [[open world assumption]].

Line 265:

==Programs with constraints==

The stable model semantics has been generalized to many kinds of logic programs other than collections of "traditional" rules discussed above&nbsp;— rulesabove—rules of the form

:<math>A \leftarrow B_{1},\dots,B_{m},\operatorname{not} C_{1},\dots,\operatorname{not} C_{n}</math>

where <math>A,B_{1},\dots,B_{m},C_{1},\dots,C_{n}</math> are atoms. One [[simple extension]] allows programs to contain ''constraints''&nbsp;— rules—rules with the empty head:

:<math>\leftarrow B_{1},\dots,B_{m},\operatorname{not}C_{1},\dots,\operatorname{not} C_{n}.</math>

Line 277:

:<math>\neg(B_{1}\land\cdots\land B_{m}\land\neg C_{1}\land\cdots\land\neg C_{n}).</math>

We can now extend the definition of a stable model to programs with constraints. As in the case of traditional programs, to define stable models, we begin with programs that do not contain negation. Such a program may be inconsistent; then we say that it has no stable models. If such a program <math>P</math> is consistent then <math>P</math> has a unique minimal model, and that model is considered the only stable model of <math>P</math>.

Next, stable models of arbitrary programs with constraints are defined using reducts, formed in the same way as in the case of traditional programs (see the [[#Definition|definition of a stable model]] above). A set <math>I</math> of atoms is a ''stable model'' of a program <math>P</math> with constraints if the reduct of <math>P</math> relative to <math>I</math> has a stable model, and that stable model equals <math>I</math>.

Line 297:

For example, the set <math>\{p,r\}</math> is a stable model of the disjunctive program

:<math>p;q\ </math>

:<math>r\leftarrow \operatorname{not} q</math>

Line 303:

because it is one of two minimal models of the reduct

:<math>p;q\ </math>

:<math>r.\ </math>

The program above has one more stable model, <math>\{q\}</math>.

Line 315:

Rules, and even [[#Disjunctive programs|disjunctive rules]], have a rather special syntactic form, in comparison with arbitrary [[propositional formula]]s. Each disjunctive rule is essentially an implication such that its [[Antecedent (logic)|antecedent]] (the body of the rule) is a conjunction of [[Literal (mathematical logic)|literals]], and its [[consequent]] (head) is a disjunction of atoms. David Pearce [1997] and Paolo Ferraris [2005] showed how to extend the definition of a stable model to sets of arbitrary propositional formulas. This generalization has applications to [[answer set programming]].

Pearce's formulation looks very different from the [[#Definition|original definition of a stable model]]. Instead of reducts, it refers to ''equilibrium logic''&nbsp;— a—a system of [[nonmonotonic logic]] based on [[Kripke semantics|Kripke models]]. Ferraris's formulation, on the other hand, is based on reducts, although the process of constructing the reduct that it uses differs from the one [[#Definition|described above]]. The two approaches to defining stable models for sets of propositional formulas are equivalent to each other.

===General definition of a stable model===

Line 323:

For instance, the reduct of the set

:<math>\{p,\ p\land q \rightarrow r,\ p \land \neg q \rightarrow s\}</math>

relative to <math>\{p,s\}</math> is

:<math>\{p,\ \bot\rightarrow \bot,\ p \land \neg\bot \rightarrow s\}.</math>

Since <math>\{p,s\}</math> is a model of the reduct, and the proper subsets of that set are not models of the reduct, <math>\{p,s\}</math> is a stable model of the given set of formulas.

Line 343:

has two stable models, <math>\empty</math> and <math>\{p\}</math>. The latter is not minimal, and it is a proper superset of the former.

Testing whether a [[finite set]] of propositional formulas has a stable model is [[Polynomial hierarchy|<math>\Sigma_2^{\rm P}</math>-complete]], as in the case of [[#Disjunctive programs|disjunctive programs]].

== See also ==

Line 355:

==References==

*{{cite book |first1=N. |last1=Bidoit |first2=C. |last2=Froidevaux |chapter=Minimalism subsumes default logic and circumscription |chapter-url= |title=Proceedings: [[Symposium on Logic in Computer Science]], Ithaca, New York, June 22-25, 1987 |publisher=IEEE Computer Society Press |date=1987 |isbn=978-0-8186-0793-6 |id=87CH2464-6 |pages=89–97 |url=}}

*{{cite book |first1=T. |last1=Eiter |first2=G. |last2=Gottlob |author2link = Georg Gottlob|chapter=Complexity results for disjunctive logic programming and application to nonmonotonic logics |chapter-url=http://www.kr.tuwien.ac.at/staff/eiter/et-archive/ilps93.ps.gz |title=ILPS '93: Proceedings of the 1993 international symposium on Logic programming |publisher=MIT Press |date=1993 |isbn=978-0-262-63152-5 |pages=266–278 }}

*{{cite journal |first1=M. |last1=van Emden |author2-link=Robert Kowalski |first2=R. |last2=Kowalski |title=The semantics of predicate logic as a programming language |journal=[[Journal of the ACM]] |volume=23 |issue= 4|pages=733–742 |date=1976 |doi=10.1145/321978.321991 |citeseerx=10.1.1.64.9246 |s2cid=11048276 |url=http://www.doc.ic.ac.uk/~rak/papers/kowalski-van_emden.pdf}}

*{{cite journal |first=F. |last=Fages |title=Consistency of Clark's completion and existence of stable models |journal=Journal of Methods of Logic in Computer Science |volume=1 |issue= |pages=51–60 |date=1994 |doi= |citeseerx=10.1.1.48.2157

|url=https://www.researchgate.net/publication/220492237}}

Line 365:

*{{cite book |first1=M. |last1=Gelfond |first2=V. |last2=Lifschitz |chapter=The stable model semantics for logic programming |chapter-url=http://www.cs.utexas.edu/users/vl/papers/stable.ps |title=Proceedings of the Fifth International Conference on Logic Programming (ICLP) |publisher=MIT Press |___location= |date=1988 |isbn=978-0-262-61054-4 |pages=1070–80 |url=}}

*{{cite journal |first1=M. |last1=Gelfond |first2=V. |last2=Lifschitz |title=Classical negation in logic programs and disjunctive databases |journal=New Generation Computing |volume=9 |issue= 3–4|pages=365–385 |date=1991 |doi=10.1007/BF03037169 |url=http://www.cs.utexas.edu/users/vl/papers/clnegdd.ps |citeseerx=10.1.1.49.9332|s2cid=13036056 }}

*{{cite journal |first1=S. |last1=Hanks |author2-link=Drew McDermott |first2=D. |last2=McDermott |title=Nonmonotonic logic and temporal projection |journal=[[Artificial Intelligence (journal)|Artificial Intelligence]]|volume=33 |issue= 3|pages=379–412 |date=1987 |doi=10.1016/0004-3702(87)90043-9 |url=https://dx.doi.org/10.1016/0004-3702%2887%2990043-9|url-access=subscription }}

*{{cite journal |first1=F. |last1=Lin |first2=Y. |last2=Zhao |title=ASSAT: Computing answer sets of a logic program by SAT solvers |journal=Artificial Intelligence |volume=157 |issue=1–2 |pages=115–137 |date=2004 |doi=10.1016/j.artint.2004.04.004 |s2cid=514581 |url=http://www.cs.ust.hk/faculty/flin/papers/assat-aij-revised.pdf}}

*{{cite book |first1=V. |last1=Marek |first2=V.S. |last2=Subrahmanian |chapter=The relationship between logic program semantics and non-monotonic reasoning |chapter-url= |title=Logic Programming: Proceedings of the Sixth International Conference |publisher=MIT Press |date=1989 |isbn=978-0-262-62065-9 |pages=600–617 |url=}}