Stable model semantics: Difference between revisions

Revision as of 16:37, 19 October 2013

Revision as of 19:34, 3 July 2014

Line 3:

==Motivation==

Research on the declarative semantics of negation in logic programming was motivated by the fact that the behavior of [[SLD_resolutionSLD resolution#SLDNF|SLDNF]] resolution—the generalization of [[SLD resolution]] used by [[Prolog]] in the presence of negation in the bodies of rules—does not fully match the [[truth tables]] familiar from classical [[propositional logic]]. Consider, for instance, the program

Research on the declarative semantics of negation in logic programming was motivated by the fact that the behavior of [[SLD_resolution#SLDNF|SLDNF]] resolution—the generalization of [[SLD resolution]] used by [[Prolog]] in the presence of negation in the bodies of rules—does not fully match the [[truth tables]] familiar from classical [[propositional logic]]. Consider, for instance, the program

:<math>p\ </math>

Line 12 ⟶ 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:

<table{| COLScols=$ WIDTHwidth="20%">

|<math>qp</math>

<td valign="top">

|<math>pq</math>

|<math>r</math>

<br>

|<math>s</math>

'''T'''

|-

</td>

|'''T'''

<td valign="top">

|'''F'''

<math>q</math>

|'''F'''.

<br>

|'''FT'''.

|}

</td>

<td valign="top">

<math>r</math>

<br>

'''F'''

</td>

<td valign="top">

<math>s</math>

<br>

'''T'''.

</td>

</table>

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>\hbox{not}</math> with negation <math>\neg,</math> and agree to treat <math>F \leftarrow G</math> as the implication <math>G \rightarrow F</math> written backwards. For instance, the last rule of the given program is, from this point of view, alternative notation for the propositional formula

Line 43 ⟶ 32:

'''T'''. In other words, that assignment is a [[model theory|model]] of the program. But this program has also other models, for instance

<table{| COLScols=$ WIDTHwidth="20%">

|<math>qp</math>

<td valign="top">

|<math>pq</math>

|<math>r</math>

<br>

|<math>s</math>

'''T'''

|-

</td>

|'''T'''.

<td valign="top">

|'''T'''

<math>q</math>

|'''T'''

<br>

|'''TF'''.

|}

</td>

<td valign="top">

<math>r</math>

<br>

'''T'''

</td>

<td valign="top">

<math>s</math>

<br>

'''F'''.

</td>

</table>

Thus one of the models of the given program is special in the sense that it correctly represents the behavior of SLDNF resolution. What are the mathematical properties of that model that make it special? An answer to this question is provided by the definition of a stable model.

correctly represents the behavior of SLDNF resolution. What are the

mathematical properties of that model that make it special? An answer to

this question is provided by the definition of a stable model.

==Relation to nonmonotonic logic==