Stable model semantics: Difference between revisions

Revision as of 15:13, 3 June 2013

Revision as of 16:37, 19 October 2013

Line 154:

===Example===

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

:<math>p\ </math>

Line 194:

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 -- 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.

Line 219:

==Relation to other theories of negation as failure==

===Program completion===

Line 246 ⟶ 247:

==Strong negation==

===Representing incomplete information===

Line 304 ⟶ 306:

:<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 310 ⟶ 312:

==Programs with constraints==

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

:<math>A \leftarrow B_{1},\dots,B_{m},\hbox{not } C_{1},\dots,\hbox{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—rules with the empty head:

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

Line 358 ⟶ 360:

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'' -- 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 378 ⟶ 380:

===Properties of the general stable model semantics===

The theorem asserting that all elements of any stable model of a program <math>P</math> are head atoms of <math>P</math> can be extended to sets of propositional formulas, if we define head atoms as follows. An atom <math>A</math> is a ''head atom'' of a set <math>P</math> of propositional formulas if at least one occurrence of <math>A</math> in a formula from <math>P</math> is neither in the scope of a negation nor in the antecedent of an implication. (We assume here that equivalence is treated as an abbreviation, not a primitive connective.)

The [[#Properties of the stable model semantics|minimality and the antichain property of stable models]] of a traditional program do not hold in the general case. For instance, (the singleton set consisting of) the formula

Line 389 ⟶ 391:

==Notes==

{{Reflist}}

==References==

* N. Bidoit and C. Froidevaux [1987] ''Minimalism subsumes default logic and circumscription''. In: Proceedings of LICS-87, pages 89-9789–97.

* T. {{Not a typo|Eiter}} and G. Gottlob [1993] ''[http://www.kr.tuwien.ac.at/staff/eiter/et-archive/ilps93.ps.gz Complexity results for disjunctive logic programming and application to nonmonotonic logics]''. In: Proceedings of ILPS-93, pages 266-278.

Line 400 ⟶ 402:

* M. van Emden and [[Robert Kowalski|R. Kowalski]] [1976] ''[http://www.doc.ic.ac.uk/~rak/papers/kowalski-van_emden.pdf The semantics of predicate logic as a programming language]''. Journal of ACM, Vol. 23, pages 733-742.

* F. Fages [1994] ''Consistency of Clark's completion and existence of stable models''. Journal of Methods of Logic in Computer Science, Vol. 1, pages 51-6051–60.

* P. Ferraris [2005] ''Answer sets for propositional theories''. In: Proceedings of LPNMR-05, pages 119-131.

Line 418 ⟶ 420:

* V. Marek and V.S. Subrahmanian [1989] ''The relationship between logic program semantics and non-monotonic reasoning''. In: Proceedings of ICLP-89, pages 600-617.

* D. Pearce [1997] ''A new logical characterization of stable models and answer sets''. In: Non-Monotonic Extensions of Logic Programming (Lecture Notes in Artificial Intelligence 1216), pages 57-7057–70.

* [[Raymond Reiter|R. Reiter]] [1980] ''A logic for default reasoning''. Artificial Intelligence, Vol. 13, pages 81-13281–132.

== See also ==