User:Michael Gelfond/Draft ASSemantics
Answer Set Semantics
[edit]Introduction
[edit]The Answer Set Semantics are a declarative, non-monotonic semantics for logic programs with negation as failure introduced by Michael Gelfond and Vladimir Lifschitz. Unlike standard Prolog, the Answer Set Semantics define the models (in this context called Answer Sets) of a logic program independently of a particular inference mechanism. In contrast with other non-monotonic logics, the Answer Set Semantics are not super-classical; Instead, they use a collection of new logical connectives.
Syntax
[edit]A program consists of a signature and a collection of rules of the form:
where 's are literals (an atom or its negation ) from . The logical connectives and are called negation as failure or default negation and epistemic disjunction respectively.
Given a rule ,
Satisfiability
[edit]A set of literals satisfies a literal if .
A set satisfies a rule if one of the following conditions hold:
Semantics
[edit]The Answer Set Semantics assigns to a logic program a collection of answer sets: consistent sets of literals over signature . Logic programs under the Answer Set Semantics may have one, many or zero answer sets.
The precise definition of the answer sets is given in two parts: first for programs whose rules do not contain default negation, and then extended to arbitrary programs using the concept of the reduct of a program.
Answer Set - Part One
[edit]Let program consists of rules of the form:
An Answer Set of is a consistent set of literals satisfying the following conditions:
- satisfies the rules of .
- is minimal. i.e. no proper subset of satisfies the rules of .
Reduct
[edit]Let by an arbitrary logic program and be a consistent set of literals.
The reduct, , of relative to is the program obtained from by:
i) removing all rules containing such that
.
ii) removing all other premises containing .
Notice that is a logic program without default negation.
Answer Set - Part Two
[edit]A consistent set of literals is an answer set for logic program if and only if is an answer set for .
Entailment
[edit]A program entails a literal , if is satisfied by every answer set of .
Answer to a Query
[edit]A logic program 's answer to a query is 'yes' if ; 'no' if and 'unknown' otherwise.