Answer set programming
From Wikipedia, the free encyclopedia
Answer set programming is a form of declarative programming that is similar in syntax to traditional logic programming and close in semantics to non-monotonic logic. The main difference between traditional logic programming and answer set programming is how negation as failure is interpreted. In traditional logic programming, negation-as-failure indicates the failure of a derivation; in answer set programming, it indicates the consistency of assumption of falsehood of a literal. It should be noted though, that in the propositional case (as it is the case in answer set programs) these two interpretation of negation (as failure) coincide.
Contents |
[edit] Syntax
A number syntactic variants exist, the syntax of answer set programs presented here follows that of Gelfond and Lifschitz presented in [1].
An answer set program is composed of a set of rules, each rule being composed of an head and a body of the form:
head :- body .
The language of rules is derived from a set of atoms which in turn may be used to form literals and extended literals. In contrast to traditional logic programming languages such as Prolog atoms are propositional rather than first-order, and can be negated using two forms of negation: classical negation (denoted by -) and negation-as-failure (denoted by not).
The head of a rule consists of a possibly empty set of literals, each literal being an atom or its classical negation (i.e. a or -a). The body of a rule consists of a possibly empty set of extended literals, each extended literal being a literal (i.e. a or -a) or a literal preceded by not, indicating negation as failure (i.e. not a or not -a).
Intuitively for a given atom a the meaning of each type of literal may be read as follows:
| Literal | Meaning |
|---|---|
a |
a can be shown to be true. |
-a |
a can be shown to be false. |
not a |
a cannot be shown to be true. |
not -a |
a cannot be shown to be false. |
If the body of the rule is empty then the rule is considered as a fact (i.e. the head of the rule is true, regardless of other rules) (this is typically written simply as head. ).
If head of the rule is empty then the rule is a constraint. In this case, if the body of the rule is satisfied then the set of atoms which lead to it being satisfied are considered to be invalid and no answer set is produced.
Answer set programs may have zero, one or many solutions (called answer sets), each consisting of a set of literals.
The following program :
a . b :- a . d :- e .
Has a single answer set { a , b }. a is in the answer set because it is a fact (first rule), b is in the answer set because, if a a is supported then b b is supported (second rule). d is not in the answer set, because e is not supported by any other rules.
The following program :
a :- not b. b :- not a. c :- a.
Has two answer sets { a , c } and { b }.
[edit] Semantics
The semantic of a program is based on its answer sets, each answer set being a set of literals. For programs not containing negation-as-failure, the semantic of a program is based on the concepts of closure and minimality:
- A program is closed under a set L of literals if the set contains at least a literal in the head of a rule whenever it contains all literals in L in its body.
- A set of literals is an answer set of a program if it is minimal (under set containment) among the ones the program is closed for.
If the program contains some literals that are negated using negation-as-failure, the semantics requires the additional concept of reduct (often referred to as the Gelfond-Lifschitz reduct from [2]):
- The reduct of a program with respect to a set of literals L is the program obtained by performing the following changes to each rule:
- remove all literals of the head that are negated using negation-as-failure and are in the set L;
- remove all literals of the tail that are negated using negation-as-failure and are not in the set L;
- remove the whole rule if it still contains negated (using negation-as-failure) atoms after the application of the two rules above.
A set of literals is an answer set of a program if it is an answer set of the reduct of the program under the set itself. In other words, an answer set can be computed by running the following nondeterministic algorithm:
choose a set of literals L; compute the reduct PL of program P with respect to L; if L is a minimal set of literals PL is closed for output L
The choice of the initial set of literals L is non-deterministic. The algorithm decides whether L is an answer set by first computing the reduct of the program under L, and then checking whether L is an answer set of this negation-as-failure-free program.
An answer set program can have zero, one, or many answer sets. A program entails a literal if all its answer sets contain that literal.
[edit] Comparison, Complexity, and Implementations
In contrast to Prolog, the semantics of answer set programs do not depend on a specific order of evaluation of the rules and of the atoms within each rule.
The complexity of checking the existence of an answer set for a program and the complexity of checking whether a program entails a literal range from P to the second level of the polynomial hierarchy depending on a set of conditions (e.g., stratification, disjunction in the head) a program may or may not satisfy.
Four systems implementing answer set programming are smodels, dlv, assat and cmodels.
[edit] See also
[edit] References
- Gelfond, Michael (1988). "The stable model semantics for logic programming". Proc. of fifth logic programming symposium.
- T. Eiter, N. Leone, C. Mateis, G. Pfeifer, F. Scarcello (1998). The KR System dlv: Progress Report, Comparisons and Benchmarks. In Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98): 406-417
- V. Lifschitz (2002). Answer set programming and plan generation. Artificial Intelligence. 138(1-2): 39-54. DOI:10.1016/S0004-3702(02)00186-8
- I. Niemela, P. Simons, T. Syrjanen (2000). Smodels: A System for Answer Set Programming. CoRR cs.AI/0003033
