The concept of a stable model, or answer set, is used to define a declarative semantics for logic programs with negation as failure. This is one of several standard approaches to the meaning of negation in logic programming, along with program completion and the well-founded semantics. The stable model semantics is the basis of answer set programming.

Motivation

Research on the declarative semantics of negation in logic programming was motivated by the fact that the behavior of 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

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

${\displaystyle s\leftarrow p,\operatorname {not} q.}$

Given this program, the query p will succeed, because the program includes p as a fact; the query q will fail, because it does not occur in the head of any of the rules. The query r will fail also, because the only rule with r in the head contains the subgoal q in its body; as we have seen, that subgoal fails. Finally, the query s succeeds, because each of the subgoals p, ${\displaystyle \operatorname {not} q}$ succeeds. (The latter succeeds because the corresponding positive goal q fails.) To sum up, the behavior of SLDNF resolution on the given program can be represented by the following truth assignment:

p	q	r	s
T	F	F	T.

On the other hand, the rules of the given program can be viewed as propositional formulas if we identify the comma with conjunction ${\displaystyle \land }$, the symbol ${\displaystyle \operatorname {not} }$ with negation ${\displaystyle \neg }$, and agree to treat ${\displaystyle F\leftarrow G}$ as the implication ${\displaystyle G\rightarrow F}$ written backwards. For instance, the last rule of the given program is, from this point of view, alternative notation for the propositional formula

${\displaystyle p\land \neg q\rightarrow s.}$

If we calculate the truth values of the rules of the program for the truth assignment shown above then we will see that each rule gets the value T. In other words, that assignment is a model of the program. But this program has also other models, for instance

p	q	r	s
T	T	T	F.

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.

Relation to nonmonotonic logic

The meaning of negation in logic programs is closely related to two theories of 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 known. Michael Gelfond proposed to read ${\displaystyle \operatorname {not} p}$ in the body of a rule as "${\displaystyle p}$ is not known", and to understand a rule with negation as the corresponding formula of autoepistemic logic. The stable model semantics, in its basic form, can be viewed as a reformulation of this idea that avoids explicit references to autoepistemic logic.

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 known. Nicole Bidoit and Christine Froidevaux proposed to treat negated atoms in the bodies of rules as justifications. For instance, the rule

${\displaystyle s\leftarrow p,\operatorname {not} q}$

can be understood as the default that allows us to derive ${\displaystyle s}$ from ${\displaystyle p}$ assuming that ${\displaystyle \neg q}$ is consistent. The stable model semantics uses the same idea, but it does not explicitly refer to default logic.

Stable models

The definition of a stable model below, reproduced from , uses two conventions. First, a truth assignment is identified with the set of atoms that get the value T. For instance, the truth assignment

p	q	r	s
T	F	F	T.

is identified with the set ${\displaystyle \{p,s\}}$. This convention allows us to use the set inclusion relation to compare truth assignments with each other. The smallest of all truth assignments ${\displaystyle \emptyset }$ is the one that makes every atom false; the largest truth assignment makes every atom true.

Second, a logic program with variables is viewed as shorthand for the set of all 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

${\displaystyle \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(X))\leftarrow \operatorname {not} \operatorname {even} (X)}$

is understood as the result of replacing X in this program by the ground terms

${\displaystyle 0,s(0),s(s(0)),\dots .}$

in all possible ways. The result is the infinite ground program

${\displaystyle \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(0))\leftarrow \operatorname {not} \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(s(0)))\leftarrow \operatorname {not} \operatorname {even} (s(0))}$

${\displaystyle \dots }$

Definition

Let P be a set of rules of the form

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

where ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$ are ground atoms. If P does not contain negation (${\displaystyle n=0}$ in every rule of the program) then, by definition, the only stable model of P is its model that is minimal relative to set inclusion.^[1] (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 I of ground atoms, the reduct of P relative to I is the set of rules without negation obtained from P by first dropping every rule such that at least one of the atoms ${\displaystyle C_{i}}$ in its body

${\displaystyle B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

belongs to I, and then dropping the parts ${\displaystyle \operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$ from the bodies of all remaining rules.

We say that I is a stable model of P if I is the stable model of the reduct of P relative to I. (Since the reduct does not contain negation, its stable model has been already defined.) As the term "stable model" suggests, every stable model of P is a model of P.

Example

To illustrate these definitions, let us check that ${\displaystyle \{p,s\}}$ is a stable model of the program

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

Zdroj:https://en.wikipedia.org?pojem=Stable_model_semantics
Text je dostupný za podmienok Creative Commons Attribution/Share-Alike License 3.0 Unported; prípadne za ďalších podmienok. Podrobnejšie informácie nájdete na stránke Podmienky použitia.

---