Content deleted Content added
added Category:Model theory using HotCat |
No edit summary |
||
Line 7:
:<math>p\ </math>
:<math>r \leftarrow p,\ q</math>
:<math>s \leftarrow p,\ \
Given this program, the query <math>p</math> will succeed, because the program includes <math>p</math> as a fact; the query <math>q</math> will fail, because it does not occur in the head of any of the rules. The query <math>r</math> will fail also, because the only rule with <math>r</math> in the head contains the subgoal <math>q</math> in its body; as we have seen, that subgoal fails. Finally, the query <math>s</math> succeeds, because each of the subgoals <math>p</math>, <math>\
{| cellpadding=5 style="width:18em"
Line 23:
|}
On the other hand, the rules of the given program can be viewed as [[propositional formula]]s if we identify the comma with conjunction <math>\land</math>, the symbol <math>\
:<math>p \land \neg q \rightarrow s.</math>
Line 47:
The meaning of negation in logic programs is closely related to two theories of [[Nonmonotonic logic|nonmonotonic reasoning]] — [[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 believed. Michael Gelfond [1987] proposed to read <math>\
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 believed. 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,\ \
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 75:
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 \
is understood as the result of replacing <math>X</math> in this program by the ground terms
Line 85:
in all possible ways. The result is the infinite ground program
:<math>\operatorname{even}(0)\ </math>
:<math>\operatorname{even}(s(0))\leftarrow \
:<math>\operatorname{even}(s(s(0)))\leftarrow \
:<math>\dots</math>
Line 97:
Let <math>P</math> be a set of rules of the form
:<math>A \leftarrow B_{1},\dots,B_{m},\
where <math>A,B_{1},\dots,B_{m},C_{1},\dots,C_{n}</math> are ground atoms. If <math>P</math> does not contain negation (<math>n=0</math> in every rule of the program) then, by definition, the only stable model of <math>P</math> 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]] [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.
Line 103:
For any set <math>I</math> of ground atoms, the ''reduct'' of <math>P</math> relative to <math>I</math> is the set of rules without negation obtained from <math>P</math> by first dropping every rule such that at least one of the atoms <math>C_i</math> in its body
:<math>B_{1},\dots,B_{m},\
belongs to <math>I</math>, and then dropping the parts <math>\
We say that <math>I</math> is a ''stable model'' of <math>P</math> if <math>I</math> is the stable model of the reduct of <math>P</math> relative to <math>I</math>. (Since the reduct does not contain negation, its stable model has been already defined.) As the term "stable model" suggests, every stable model of <math>P</math> is a model of <math>P</math>.
Line 117:
:<math>r \leftarrow p,\ q</math>
:<math>s \leftarrow p,\ \
The reduct of this program relative to <math>\{p,s\}</math> is
Line 127:
:<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>\
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
Line 141:
A program with negation may have many stable models or no stable models. For instance, the program
:<math>p \leftarrow \
:<math>q \leftarrow \
has two stable models <math>\{p\}</math>, <math>\{q\}</math>. The one-rule program
:<math>p \leftarrow \
has no stable models.
Line 159:
In this section, as in the [[#Definition|definition of a stable model]] above, by a logic program we mean a set of rules of the form
:<math>A \leftarrow B_{1},\dots,B_{m},\
where <math>A,B_{1},\dots,B_{m},C_{1},\dots,C_{n}</math> are ground atoms.
Line 187:
The [[well-founded semantics|well-founded model]] of a logic program partitions all ground atoms into three sets: true, false and unknown. If an atom is true in the well-founded model of <math>P</math> then it belongs to every stable model of <math>P</math>. The converse, generally, does not hold. For instance, the program
:<math>p \leftarrow \
:<math>q \leftarrow \
:<math>r\leftarrow p</math>
Line 219:
To incorporate strong negation in the theory of stable models, Gelfond and Lifschitz [1991] allowed each of the expressions <math>A</math>, <math>B_i</math>, <math>C_i</math> in a rule
:<math>A \leftarrow B_{1},\dots,B_{m},\
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.
Line 227:
For instance, the program
:<math>p \leftarrow \
:<math>q \leftarrow \
:<math>r\ </math>
:<tt><math>\sim r\leftarrow \
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>.
Line 241:
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\
(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
Line 249:
:<math>p(c,d)\ </math>
:<math>\sim p(X,Y)\leftarrow\
consists of 2 positive atoms
Line 267:
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
:<math>A \leftarrow B_{1},\dots,B_{m},\
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},\
Recall that a traditional rule can be viewed as alternative notation for a propositional formula if we identify the comma with conjunction <math>\land</math>, the symbol <math>\
:<math>\neg(B_{1}\land\cdots\land B_{m}\land\neg C_{1}\land\cdots\land\neg C_{n}).</math>
Line 289:
In a ''disjunctive rule'', the head may be the disjunction of several atoms:
:<math>A_1;\dots;A_k \leftarrow B_{1},\dots,B_{m},\
(the semicolon is viewed as alternative notation for disjunction <math>\lor</math>). Traditional rules correspond to <math>k=1</math>, and [[#Programs with constraints|constraints]] to <math>k=0</math>. To extend the stable model semantics to disjunctive programs [Gelfond and Lifschitz, 1991], we first define that in the absence of negation (<math>n=0</math> in each rule) the stable models of a program are its minimal models. The definition of the reduct for disjunctive programs remains [[#Definition|the same as before]]. A set <math>I</math> of atoms is a ''stable model'' of <math>P</math> if <math>I</math> is a stable model of the reduct of <math>P</math> relative to <math>I</math>.
Line 297:
:<math>p;q\ </math>
:<math>r\leftarrow \
because it is one of two minimal models of the reduct
Line 350:
* N. Bidoit and C. Froidevaux [1987] ''Minimalism subsumes default logic and circumscription''. In: Proceedings of LICS-87, pages 89–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
* 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
* 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–60.
* P. Ferraris [2005] ''Answer sets for propositional theories''. In: Proceedings of LPNMR-05, pages
* P. Ferraris and V. Lifschitz [2005] ''[http://www.cs.utexas.edu/users/vl/papers/mfasp.ps Mathematical foundations of answer set programming]''. In: We Will Show Them! Essays in Honour of Dov Gabbay, King's College Publications, pages
* M. Gelfond [1987] ''[https://www.aaai.org/Papers/AAAI/1987/AAAI87-037.pdf On stratified autoepistemic theories]''. In: Proceedings of AAAI-87, pages
* M. Gelfond and V. Lifschitz [1988] ''[http://www.cs.utexas.edu/users/vl/papers/stable.ps The stable model semantics for logic programming]''. In: Proceedings of the Fifth International Conference on Logic Programming (ICLP), pages
* M. Gelfond and V. Lifschitz [1991] ''[http://www.cs.utexas.edu/users/vl/papers/clnegdd.ps Classical negation in logic programs and disjunctive databases]''. New Generation Computing, Vol. 9, pages
* S. Hanks and [[Drew McDermott|D. McDermott]] [1987] ''Nonmonotonic logic and temporal projection''. Artificial Intelligence, Vol. 33, pages
* F. Lin and Y. Zhao [2004] ''[http://www.cs.ust.hk/faculty/flin/papers/assat-aij-revised.pdf ASSAT: Computing answer sets of a logic program by SAT solvers]''. Artificial Intelligence, Vol. 157, pages
* V. Marek and V.S. Subrahmanian [1989] ''The relationship between logic program semantics and non-monotonic reasoning''. In: Proceedings of ICLP-89, pages
* 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–70.
* [[Raymond Reiter|R. Reiter]] [1980] ''A logic for default reasoning''. Artificial Intelligence, Vol. 13, pages 81–132.
| |||