Negation As Failure - Autoepistemic Semantics

Autoepistemic Semantics

The completion semantics justifies interpreting the result of a NAF inference as the classical negation of . However, Michael Gelfond showed that it is also possible to interpret literally as " can not be shown", " is not known" or " is not believed", as in autoepistemic logic. The autoepistemic interpretation was developed further by Gelfond and Lifschitz and is the basis of answer set programming.

The autoepistemics semantics of a pure Prolog program P with NAF literals is obtained by "expanding" P with a set of ground (variable-free) NAF literals Δ that is stable in the sense that

Δ = { | is not implied by P ∪ Δ}

In other words, a set of assumptions Δ about what can not be shown is stable if and only if Δ is the set of all sentences that truly can not be shown from the program P expanded by Δ. Here, because of the simple syntax of pure Prolog programs, "implied by" can be understood very simply as derivability using modus ponens and universal instantiation alone.

A program can have zero, one or more stable expansions. For example

has no stable expansions.

has exactly one stable expansion Δ = {}

has exactly two stable expansions Δ₁ = {} and Δ₂ = {}.

The autoepistemic interpretation of NAF can be combined with classical negation, as in extended logic programming and answer set programming. Combining the two negations, it is possible to express, for example

(the closed world assumption) and

( holds by default).