Stable model semantics
Encyclopedia
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
.
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
Given this program, the query
will succeed, because the program includes 
as a fact; the query 
will fail, because it does not occur in the head of any of the rules. The query 
will fail also, because the only rule with 
in the head contains the subgoal 
in its body; as we have seen, that subgoal fails. Finally, the query 
succeeds, because each of the subgoals 
, 
succeeds. (The latter succeeds because the corresponding positive goal 
fails.) To sum up, the behavior of SLDNF resolution on the given program can be represented by the following truth assignment:
On the other hand, the rules of the given program can be viewed as propositional formula
s if we identify the comma with conjunction
the symbol 
with negation 
and agree to treat 
as the implication 
written backwards. For instance, the last rule of the given program is, from this point of view, alternative notation for the propositional formula
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
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.
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 believed.
Michael Gelfond [1987] proposed to read
in the body of a rule as "
is not believed", 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 believed. Nicole Bidoit and Christine Froidevaux [1987] proposed to treat negated atoms in the bodies of rules as justifications. For instance, the rule
can be understood as the default that allows us to derive
from 
assuming that 
is consistent. The stable model semantics uses the same idea, but it does not explicitly refer to default logic.
is identified with the set
. This convention allows us to use the set inclusion relation to compare truth assignments with each other. The smallest of all truth assignments 
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
is understood as the result of replacing
in this program by the ground terms
in all possible ways. The result is the infinite ground program
be a set of rules of the form
where
are ground atoms. If 
does not contain negation (
in
every rule of the program) then, by definition, the only stable model of
is its model that is minimal relative to set inclusion. (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
of ground atoms, the reduct of 
relative to 
is the set of rules without negation obtained from 
by first dropping every rule such that at least one of the atoms 
in its body
belongs to
, and then dropping the parts
from the bodies of all remaining rules.
We say that
is a stable model of 
if 
is the stable model of the reduct of 
relative to 
. (Since the reduct does not contain negation, its stable model has been already defined.) As the term "stable model" suggests, every stable model of 
is a model of 
.
is a stable model of the program
The reduct of this program relative to
is
(Indeed, since
, the reduct is obtained from the program by dropping the part 
) The stable model of the reduct is 
. (Indeed, this set of atoms satisfies every rule of the reduct, and it has no proper subsets with the same property.) Thus after computing the stable model of the reduct we arrived at the same set 
that we started with. Consequently, that set is a stable model.
Checking in the same way the other 15 sets consisting of the atoms
shows that this program has no other stable models. For instance, the reduct of the program relative to 
is
The stable model of the reduct is
, which is different from the set 
that we started with.
has two stable models
, 
. The one-rule program
has no stable models.
If we think of the stable model semantics as a description of the behavior of Prolog
in the presence of negation then programs without a unique stable model can be judged unsatisfactory: they do not provide an unambiguous specification for Prolog-style query answering. For instance, the two programs above are not reasonable as Prolog programs -- SLDNF resolution does not terminate on them.
But the use of stable models in answer set programming
provides a different perspective on such programs. In that programming paradigm, a given search problem is represented by a logic program so that the stable models of the program correspond to solutions.
Then programs with many stable models correspond to problems with many solutions, and programs without stable models correspond to unsolvable problems. For instance, the eight queens puzzle
has 92 solutions; to solve it using answer set programming, we encode it by a logic program with 92 stable models. From this point of view, logic programs with exactly one stable model are rather special in answer set programming, like polynomials with exactly one root in algebra.
where
are ground atoms.
Head atoms:
If an atom
belongs to a stable model of a logic program 
then 
is the head of one of the rules of 
.
Minimality: Any stable model of a logic program
is minimal among the models of 
relative to set inclusion.
The antichain property:
If
and 
are stable models of the same logic program then 
is not a proper subset of 
. In other words, the set of stable models of a program is an antichain
.
NP-completeness:
Testing whether a finite ground logic program has a stable model is NP-complete
.
is the tautology
. The model 
of this tautology is stable, but its other model 
is not. François Fages [1994] found a syntactic condition on logic programs that eliminates such counterexamples and guarantees the stability of every model of the program's completion. The programs that satisfy his condition are called tight.
Fangzhen Lin and Yuting Zhao [2004] showed how to make the completion of a nontight program stronger so that all its nonstable models will be eliminated. The additional formulas that they add to the completion are called loop formulas.
of a logic program partitions all ground atoms into three sets: true, false and unknown. If an atom is true in the well-founded model of
then it belongs to every stable model of 
. The converse, generally, does not hold. For instance, the program
has two stable models,
and 
. Even though 
belongs to both of them, its value in the well-founded model is unknown.
Furthermore, if an atom is false in the well-founded model of a program then it does not belong to any of its stable models. Thus the well-founded model of a logic program provides a lower bound on the intersection of its stable models and an upper bound on their union.
, a set of ground atoms can be thought of as a description of a complete state of knowledge: the atoms that belong to the set are known to be true, and the atoms that do not belong to the set are known to be false. A possibly incomplete state of knowledge can be described using a consistent but possibly incomplete set of literals; if an atom
does not belong to the set and its negation does not belong to the set either then it is not known whether 
is true.
In the context of logic programming, this idea leads to the need to distinguish between two kinds of negation -- negation as failure, discussed above, and strong negation, which is denoted here by
. The following example, illustrating the difference between the two kinds of negation, belongs to John McCarthy
. A school bus may cross railway tracks under the condition that there is no approaching train. If we do not necessarily know whether a train is approaching then the rule using negation as failure
is not an adequate representation of this idea: it says that it's okay to cross in the absence of information about an approaching train. The weaker rule, that uses strong negation in the body, is preferable:
It says that it's okay to cross if we know that no train is approaching.
, 
, 
in a rule
to be either an atom or an atom prefixed with the strong negation symbol. Instead of stable models, this generalization uses answer sets, which may include both atoms and atoms prefixed with strong negation.
An alternative approach [Ferraris and Lifschitz, 2005] treats strong negation as a part of an atom, and it does not require any changes in the definition of a stable model. In this theory of strong negation, we distinguish between atoms of two kinds, positive and negative, and assume that each negative atom is an expression of the form
, where 
is a positive atom. A set of atoms is called coherent if it does not contain "complementary" pairs of atoms 
. Coherent stable models of a program are identical to its consistent answer sets in the sense of [Gelfond and Lifschitz, 1991].
For instance, the program
has two stable models,
and 
. The first model is coherent; the second is not, because it contains both the atom 
and the atom 
.
for a predicate
can be expressed by the rule
(the relation
does not hold for a tuple 
if there is no evidence that it does). For instance, the stable model of the program
consists of 2 positive atoms
and 14 negative atoms
-- the strong negations of all other positive ground atoms formed from
.
A logic program with strong negation can include the closed world assumption rules for some of its predicates and leave the other predicates in the realm of the open world assumption
.
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 
.
(the semicolon is viewed as alternative notation for disjunction
). Traditional rules correspond to 
, and constraints to 
. To extend the stable model semantics to disjunctive programs [Gelfond and Lifschitz, 1991], we first define that in the absence of negation (
in each rule) the stable models of a program are its minimal models. The definition of the reduct for disjunctive programs remains the same as before. A set 
of atoms is a stable model of 
if 
is a stable model of the reduct of 
relative to 
.
For example, the set
is a stable model of the disjunctive program
because it is one of two minimal models of the reduct
The program above has one more stable model,
.
As in the case of traditional programs, each element of any stable model of a disjunctive program
is a head atom of 
, in the sense that it occurs in the head of one of the rules of 
. As in the traditional case, the stable models of a disjunctive program are minimal and form an antichain. Testing whether a finite disjunctive program has a stable model is 
-complete
[Eiter and Gottlob, 1993].
s. Each disjunctive rule is essentially an implication such that its antecedent
(the body of the rule) is a conjunction of literals
, and its consequent
(head) is a disjunction of atoms. David Pearce [1997] and Paolo Ferraris [2005] showed how to extend the definition of a stable model to sets of arbitrary propositional formulas. This generalization has applications to answer set programming
.
Pearce's formulation looks very different from the original definition of a stable model. Instead of reducts, it refers to equilibrium logic -- a system of nonmonotonic logic based on Kripke models
. Ferraris's formulation, on the other hand, is based on reducts, although the process of constructing the reduct that it uses differs from the one described above. The two approaches to defining stable models for sets of propositional formulas are equivalent to each other.
relative to a set 
of atoms is the formula obtained from 
by replacing each maximal subformula that is not satisfied by 
with the logical constant 
(false). The reduct of a set 
of propositional formulas relative to 
consists of the reducts of all formulas from 
relative to 
. As in the case of disjunctive programs, we say that a set 
of atoms is a stable model of 
if 
is minimal (with respect to set inclusion) among the models of the reduct of 
relative to 
.
For instance, the reduct of the set
relative to
is
Since
is a model of the reduct, and the proper subsets of that set are not models of the reduct,
is a stable model of the given set of formulas.
We have seen that
is also a stable model of the same formula, written in logic programming notation, in the sense of the original definition. This is an instance of a general fact: in application to a set of (formulas corresponding to) traditional rules, the definition of a stable model according to Ferraris is equivalent to the original definition. The same is true, more generally, for programs with constraints and for disjunctive programs.
are head atoms of 
can be extended to sets of propositional formulas, if we define head atoms as follows. An atom 
is a head atom of a set 
of propositional formulas if at least one occurrence of 
in a formula from 
is neither in the scope of a negation nor in the antecedent of an implication. (We assume here that equivalence is treated as an abbreviation, not a primitive connective.)
The minimality and the antichain property of stable models of a traditional program do not hold in the general case. For instance, (the singleton set consisting of) the formula
has two stable models,
and 
. The latter is not minimal, and it is a proper superset of the former.
Testing whether a finite set of propositional formulas has a stable model is
-complete
, as in the case of disjunctive programs.
Logic programming
Logic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a...
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
Well-founded semantics
In logic programming, the well-founded semantics is one definition of how we can make conclusions from a set of logical rules. In logic programming, we give a computer a set of facts, and a set of "inference rules" about how these facts relate...
. The stable model semantics is the basis of
answer set programming
Answer set programming
Answer set programming is a form of declarative programming oriented towards difficult search problems. It is based on the stable model semantics of logic programming. In ASP, search problems are reduced to computing stable models, and answer set solvers -- programs for generating stable...
.
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 resolutionSLD resolution
SLD resolution is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.-The SLD inference rule:...
used by Prolog
Prolog
Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
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
Given this program, the query
will succeed, because the program includes as a fact; the query will fail, because it does not occur in the head of any of the rules. The query will fail also, because the only rule with in the head contains the subgoal in its body; as we have seen, that subgoal fails. Finally, the query succeeds, because each of the subgoals , succeeds. (The latter succeeds because the corresponding positive goal fails.) To sum up, the behavior of SLDNF resolution on the given program can be represented by the following truth assignment: T |  F |  F |  T. |
On the other hand, the rules of the given program can be viewed as propositional formula
Propositional formula
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value...
s if we identify the comma with conjunction
the symbol with negation and agree to treat as the implication written backwards. For instance, the last rule of the given program is, from this point of view, alternative notation for the propositional formulaIf 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
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
of the program. But this program has also other models, for instance
 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
Autoepistemic logic
The autoepistemic logic is a formal logic for the representation and reasoning of knowledge about knowledge. While propositional logic can only express facts, autoepistemic logic can express knowledge and lack of knowledge about facts....
and default logic
Default logic
Default logic is a non-monotonic logic proposed by Raymond Reiter to formalize reasoning with default assumptions.Default logic can express facts like “by default, something is true”; by contrast, standard logic can only express that something is true or that something is false...
. 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
Modal operator
In modal logic, a modal operator is an operator which forms propositions from propositions. In general, a modal operator has the "formal" property of being non-truth-functional, and is "intuitively" characterised by expressing a modal attitude about the proposition to which the operator is applied...
that allows us to distinguish between what is true and what is believed.
Michael Gelfond [1987] proposed to read
in the body of a rule as " is not believed", 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 believed. Nicole Bidoit and Christine Froidevaux [1987] proposed to treat negated atoms in the bodies of rules as justifications. For instance, the rule
can be understood as the default that allows us to derive
from assuming that 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 [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 T |  F |  F |  T |
is identified with the set
. This convention allows us to use the set inclusion relation to compare truth assignments with each other. The smallest of all truth assignments 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
is understood as the result of replacing
in this program by the ground termsin all possible ways. The result is the infinite ground program
Definition
Let be a set of rules of the formwhere
are ground atoms. If does not contain negation ( inevery rule of the program) then, by definition, the only stable model of
is its model that is minimal relative to set inclusion. (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
of ground atoms, the reduct of relative to is the set of rules without negation obtained from by first dropping every rule such that at least one of the atoms in its bodybelongs to
, and then dropping the parts from the bodies of all remaining rules.We say that
is a stable model of if is the stable model of the reduct of relative to . (Since the reduct does not contain negation, its stable model has been already defined.) As the term "stable model" suggests, every stable model of is a model of .Example
To illustrate these definitions, let us check that is a stable model of the programThe reduct of this program relative to
is(Indeed, since
, the reduct is obtained from the program by dropping the part ) The stable model of the reduct is . (Indeed, this set of atoms satisfies every rule of the reduct, and it has no proper subsets with the same property.) Thus after computing the stable model of the reduct we arrived at the same set that we started with. Consequently, that set is a stable model.Checking in the same way the other 15 sets consisting of the atoms
shows that this program has no other stable models. For instance, the reduct of the program relative to isThe stable model of the reduct is
, which is different from the set that we started with.Programs without a unique stable model
A program with negation may have many stable models or no stable models. For instance, the programhas two stable models
, . The one-rule programhas no stable models.
If we think of the stable model semantics as a description of the behavior of Prolog
Prolog
Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
in the presence of negation then programs without a unique stable model can be judged unsatisfactory: they do not provide an unambiguous specification for Prolog-style query answering. For instance, the two programs above are not reasonable as Prolog programs -- SLDNF resolution does not terminate on them.
But the use of stable models in answer set programming
Answer set programming
Answer set programming is a form of declarative programming oriented towards difficult search problems. It is based on the stable model semantics of logic programming. In ASP, search problems are reduced to computing stable models, and answer set solvers -- programs for generating stable...
provides a different perspective on such programs. In that programming paradigm, a given search problem is represented by a logic program so that the stable models of the program correspond to solutions.
Then programs with many stable models correspond to problems with many solutions, and programs without stable models correspond to unsolvable problems. For instance, the eight queens puzzle
Eight queens puzzle
The eight queens puzzle is the problem of placing eight chess queens on an 8×8 chessboard so that no two queens attack each other. Thus, a solution requires that no two queens share the same row, column, or diagonal...
has 92 solutions; to solve it using answer set programming, we encode it by a logic program with 92 stable models. From this point of view, logic programs with exactly one stable model are rather special in answer set programming, like polynomials with exactly one root in algebra.
Properties of the stable model semantics
In this section, as in the definition of a stable model above, by a logic program we mean a set of rules of the formwhere
are ground atoms.Head atoms:
If an atom
belongs to a stable model of a logic program then is the head of one of the rules of .Minimality: Any stable model of a logic program
is minimal among the models of relative to set inclusion.The antichain property:
If
and are stable models of the same logic program then is not a proper subset of . In other words, the set of stable models of a program is an antichainAntichain
In mathematics, in the area of order theory, an antichain is a subset of a partially ordered set such that any two elements in the subset are incomparable. Let S be a partially ordered set...
.
NP-completeness:
Testing whether a finite ground logic program has a stable model is NP-complete
NP-complete
In computational complexity theory, the complexity class NP-complete is a class of decision problems. A decision problem L is NP-complete if it is in the set of NP problems so that any given solution to the decision problem can be verified in polynomial time, and also in the set of NP-hard...
.
Program completion
Any stable model of a finite ground program is not only a model of the program itself, but also a model of its completion [Marek and Subrahmanian, 1989]. The converse, however, is not true. For instance, the completion of the one-rule programis the tautology
Tautology (logic)
In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...
. The model of this tautology is stable, but its other model is not. François Fages [1994] found a syntactic condition on logic programs that eliminates such counterexamples and guarantees the stability of every model of the program's completion. The programs that satisfy his condition are called tight.Fangzhen Lin and Yuting Zhao [2004] showed how to make the completion of a nontight program stronger so that all its nonstable models will be eliminated. The additional formulas that they add to the completion are called loop formulas.
Well-founded semantics
The well-founded modelWell-founded semantics
In logic programming, the well-founded semantics is one definition of how we can make conclusions from a set of logical rules. In logic programming, we give a computer a set of facts, and a set of "inference rules" about how these facts relate...
of a logic program partitions all ground atoms into three sets: true, false and unknown. If an atom is true in the well-founded model of
then it belongs to every stable model of . The converse, generally, does not hold. For instance, the programhas two stable models,
and . Even though belongs to both of them, its value in the well-founded model is unknown.Furthermore, if an atom is false in the well-founded model of a program then it does not belong to any of its stable models. Thus the well-founded model of a logic program provides a lower bound on the intersection of its stable models and an upper bound on their union.
Representing incomplete information
From the perspective of knowledge representationKnowledge representation
Knowledge representation is an area of artificial intelligence research aimed at representing knowledge in symbols to facilitate inferencing from those knowledge elements, creating new elements of knowledge...
, a set of ground atoms can be thought of as a description of a complete state of knowledge: the atoms that belong to the set are known to be true, and the atoms that do not belong to the set are known to be false. A possibly incomplete state of knowledge can be described using a consistent but possibly incomplete set of literals; if an atom
does not belong to the set and its negation does not belong to the set either then it is not known whether is true.In the context of logic programming, this idea leads to the need to distinguish between two kinds of negation -- negation as failure, discussed above, and strong negation, which is denoted here by
. The following example, illustrating the difference between the two kinds of negation, belongs to John McCarthyJohn McCarthy (computer scientist)
John McCarthy was an American computer scientist and cognitive scientist. He coined the term "artificial intelligence" , invented the Lisp programming language and was highly influential in the early development of AI.McCarthy also influenced other areas of computing such as time sharing systems...
. A school bus may cross railway tracks under the condition that there is no approaching train. If we do not necessarily know whether a train is approaching then the rule using negation as failure
is not an adequate representation of this idea: it says that it's okay to cross in the absence of information about an approaching train. The weaker rule, that uses strong negation in the body, is preferable:
It says that it's okay to cross if we know that no train is approaching.
Coherent stable models
To incorporate strong negation in the theory of stable models, Gelfond and Lifschitz [1991] allowed each of the expressions, , in a ruleto be either an atom or an atom prefixed with the strong negation symbol. Instead of stable models, this generalization uses answer sets, which may include both atoms and atoms prefixed with strong negation.
An alternative approach [Ferraris and Lifschitz, 2005] treats strong negation as a part of an atom, and it does not require any changes in the definition of a stable model. In this theory of strong negation, we distinguish between atoms of two kinds, positive and negative, and assume that each negative atom is an expression of the form
, where is a positive atom. A set of atoms is called coherent if it does not contain "complementary" pairs of atoms . Coherent stable models of a program are identical to its consistent answer sets in the sense of [Gelfond and Lifschitz, 1991].For instance, the program
has two stable models,
and . The first model is coherent; the second is not, because it contains both the atom and the atom .Closed world assumption
According to [Gelfond and Lifschitz, 1991], the closed world assumptionClosed world assumption
The closed world assumption is the presumption that what is not currently known to be true, is false. The same name also refers to a logical formalization of this assumption by Raymond Reiter. The opposite of the closed world assumption is the open world assumption , stating that lack of knowledge...
for a predicate
can be expressed by the rule(the relation
does not hold for a tuple if there is no evidence that it does). For instance, the stable model of the programconsists of 2 positive atoms
and 14 negative atoms
-- the strong negations of all other positive ground atoms formed from
.A logic program with strong negation can include the closed world assumption rules for some of its predicates and leave the other predicates in the realm of the open world assumption
Open World Assumption
In formal logic, the open world assumption is the assumption that the truth-value of a statement is independent of whether or not it is known by any single observer or agent to be true. It is the opposite of the closed world assumption, which holds that any statement that is not known to be true is...
.
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 formwhere
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
Answer set programming
Answer set programming is a form of declarative programming oriented towards difficult search problems. It is based on the stable model semantics of logic programming. In ASP, search problems are reduced to computing stable models, and answer set solvers -- programs for generating stable...
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 .Disjunctive programs
In a disjunctive rule, the head may be the disjunction of several atoms:(the semicolon is viewed as alternative notation for disjunction
). Traditional rules correspond to , and constraints to . To extend the stable model semantics to disjunctive programs [Gelfond and Lifschitz, 1991], we first define that in the absence of negation ( in each rule) the stable models of a program are its minimal models. The definition of the reduct for disjunctive programs remains the same as before. A set of atoms is a stable model of if is a stable model of the reduct of relative to .For example, the set
is a stable model of the disjunctive programbecause it is one of two minimal models of the reduct
The program above has one more stable model,
.As in the case of traditional programs, each element of any stable model of a disjunctive program
is a head atom of , in the sense that it occurs in the head of one of the rules of . As in the traditional case, the stable models of a disjunctive program are minimal and form an antichain. Testing whether a finite disjunctive program has a stable model is -completePolynomial hierarchy
In computational complexity theory, the polynomial hierarchy is a hierarchy of complexity classes that generalize the classes P, NP and co-NP to oracle machines...
[Eiter and Gottlob, 1993].
Stable models of a set of propositional formulas
Rules, and even disjunctive rules, have a rather special syntactic form, in comparison with arbitrary propositional formulaPropositional formula
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value...
s. Each disjunctive rule is essentially an implication such that its antecedent
Antecedent (logic)
An antecedent is the first half of a hypothetical proposition.Examples:* If P, then Q.This is a nonlogical formulation of a hypothetical proposition...
(the body of the rule) is a conjunction of literals
Literal (mathematical logic)
In mathematical logic, a literal is an atomic formula or its negation.The definition mostly appears in proof theory , e.g...
, and its consequent
Consequent
A consequent is the second half of a hypothetical proposition. In the standard form of such a proposition, it is the part that follows "then".Examples:* If P, then Q.Q is the consequent of this hypothetical proposition....
(head) is a disjunction of atoms. David Pearce [1997] and Paolo Ferraris [2005] showed how to extend the definition of a stable model to sets of arbitrary propositional formulas. This generalization has applications to answer set programming
Answer set programming
Answer set programming is a form of declarative programming oriented towards difficult search problems. It is based on the stable model semantics of logic programming. In ASP, search problems are reduced to computing stable models, and answer set solvers -- programs for generating stable...
.
Pearce's formulation looks very different from the original definition of a stable model. Instead of reducts, it refers to equilibrium logic -- a system of nonmonotonic logic based on Kripke models
Kripke semantics
Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...
. Ferraris's formulation, on the other hand, is based on reducts, although the process of constructing the reduct that it uses differs from the one described above. The two approaches to defining stable models for sets of propositional formulas are equivalent to each other.
General definition of a stable model
According to [Ferraris, 2005], the reduct of a propositional formula relative to a set of atoms is the formula obtained from by replacing each maximal subformula that is not satisfied by with the logical constant (false). The reduct of a set of propositional formulas relative to consists of the reducts of all formulas from relative to . As in the case of disjunctive programs, we say that a set of atoms is a stable model of if is minimal (with respect to set inclusion) among the models of the reduct of relative to .For instance, the reduct of the set
relative to
isSince
is a model of the reduct, and the proper subsets of that set are not models of the reduct, is a stable model of the given set of formulas.We have seen that
is also a stable model of the same formula, written in logic programming notation, in the sense of the original definition. This is an instance of a general fact: in application to a set of (formulas corresponding to) traditional rules, the definition of a stable model according to Ferraris is equivalent to the original definition. The same is true, more generally, for programs with constraints and for disjunctive programs.Properties of the general stable model semantics
The theorem asserting that all elements of any stable model of a program are head atoms of can be extended to sets of propositional formulas, if we define head atoms as follows. An atom is a head atom of a set of propositional formulas if at least one occurrence of in a formula from is neither in the scope of a negation nor in the antecedent of an implication. (We assume here that equivalence is treated as an abbreviation, not a primitive connective.)The minimality and the antichain property of stable models of a traditional program do not hold in the general case. For instance, (the singleton set consisting of) the formula
has two stable models,
and . The latter is not minimal, and it is a proper superset of the former.Testing whether a finite set of propositional formulas has a stable model is
-completePolynomial hierarchy
In computational complexity theory, the polynomial hierarchy is a hierarchy of complexity classes that generalize the classes P, NP and co-NP to oracle machines...
, as in the case of disjunctive programs.