Completion Semantics
The semantics of NAF remained an open issue until Keith Clark showed that it is correct with respect to the completion of the logic program, where, loosely speaking, "only" and are interpreted as "if and only if", written as "iff" or "".
For example, the completion of the four clauses above is
The NAF inference rule simulates reasoning explicitly with the completion, where both sides of the equivalence are negated and negation on the right-hand side is distributed down to atomic formulae. For example, to show, NAF simulates reasoning with the equivalences
In the non-propositional case, the completion needs to be augmented with equality axioms, to formalise the assumption that individuals with distinct names are distinct. NAF simulates this by failure of unification. For example, given only the two clauses
- t
NAF derives .
The completion of the program is
augmented with unique names axioms and domain closure axioms.
The completion semantics is closely related both to circumscription and to the closed world assumption.
Read more about this topic: Negation As Failure