|
The definition of a stable model below, reproduced from [Gelfond and Lifschitz, 1988], uses two conventions. First, a truth assignment is identified with the set of atoms that get the value '''T'''. For instance, the truth assignment
:{| cellpadding=5 style="width:18em"
|{{mvar|p}}
|<math>p</math>
|{{mvar|q}}
|<math>q</math>
|{{mvar|r}}
|<math>r</math>
|{{mvar|s}}
|<math>s</math>
|-
|'''T'''
:<math>\operatorname{even}(s(X))\leftarrow \operatorname{not} \operatorname{even}(X)</math>
is understood as the result of replacing <math>{{mvar|X</math>}} in this program by the ground terms
:<math>0,\ s(0),\ s(s(0)),\dots.</math>
===Definition===
Let <math>{{mvar|P</math>}} be a set of 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 ground atoms. If <math>{{mvar|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>{{mvar|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.
For any set <math>{{mvar|I</math>}} of ground atoms, the ''reduct'' of <math>{{mvar|P</math>}} relative to <math>{{mvar|I</math>}} is the set of rules without negation obtained from <math>{{mvar|P</math>}} by first dropping every rule such that at least one of the atoms <math>{{mvar|C_i</math>}} in its body
:<math>B_{1},\dots,B_{m},\operatorname{not} C_{1},\dots,\operatorname{not} C_{n}</math>
belongs to <math>{{mvar|I</math>}}, and then dropping the parts <math>\operatorname{not} C_{1},\dots,\operatorname{not} C_{n}</math> from the bodies of all remaining rules.
We say that <math>{{mvar|I</math>}} is a ''stable model'' of <math>{{mvar|P</math>}} if <math>{{mvar|I</math>}} is the stable model of the reduct of <math>{{mvar|P</math>}} relative to <math>{{mvar|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>{{mvar|P</math>}} is a model of <math>{{mvar|P</math>}}.
===Example===
| 