Stable Model Semantics - Programs With Constraints

Programs With Constraints

The stable model semantics has been generalized to many kinds of logic programs other than collections of "traditional" rules discussed above -- rules of the form

where are atoms. One simple extension allows programs to contain constraints -- rules with the empty head:

Recall that a traditional rule can be viewed as alternative notation for a propositional formula if we identify the comma with conjunction the symbol with negation and agree to treat as the implication written backwards. To extend this convention to constraints, we identify a constraint with the negation of the formula corresponding to its body:

We can now extend the definition of a stable model to programs with constraints. As in the case of traditional programs, we begin with programs that do not contain negation. Such a program may be inconsistent; then we say that it has no stable models. If such a program is consistent then has a unique minimal model, and that model is considered the only stable model of .

Next, stable models of arbitrary programs with constraints are defined using reducts, formed in the same way as in the case of traditional programs (see the definition of a stable model above.) A set of atoms is a stable model of a program with constraints if the reduct of relative to has a stable model, and that stable model equals .

The properties of the stable model semantics stated above for traditional programs hold in the presence of constraints as well.

Constraints play an important role in answer set programming because adding a constraint to a logic program affects the collection of stable models of in a very simple way: it eliminates the stable models that violate the constraint. In other words, for any program with constraints and any constraint, the stable models of can be characterized as the stable models of that satisfy .