Content deleted Content added
Magioladitis (talk | contribs) →Stable models: use wikicode |
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
|<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
|<math>p</math>
|<math>q</math>
Line 65:
{| cellpadding=5
|<math>p</math>
|<math>q</math>
| |||