Content deleted Content added
No edit summary |
|||
Line 11:
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>\hbox{not } q</math> succeeds. (The latter succeeds because the corresponding positive goal <math>q</math> fails.) To sum up, the behavior of SLDNF resolution on the given program can be represented by the following truth assignment:
{| cellpadding=5 style="width:18em"
|<math>p</math>
|<math>q</math>
Line 31:
'''T'''. In other words, that assignment is a [[model theory|model]] of the program. But this program has also other models, for instance
{| cellpadding=5 style="width:18em"
|<math>p</math>
|<math>q</math>
Line 64:
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"
|<math>p</math>
|<math>q</math>
| |||