Content deleted Content added
No edit summary Tag: Reverted |
Link suggestions feature: 3 links added. |
||
| (4 intermediate revisions by 3 users not shown) | |||
Line 153:
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—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 269:
:<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''—rules with the empty head:
:<math>\leftarrow B_{1},\dots,B_{m},\operatorname{not}C_{1},\dots,\operatorname{not} C_{n}.</math>
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 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=}}
Line 372:
[[Category:Logic programming]]
| |||