HOME

TheInfoList



OR:

Negation as failure (NAF, for short) is a non-monotonic inference rule in
logic programming Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic prog ...
, used to derive \mathrm~p (i.e. that ~p is assumed not to hold) from failure to derive ~p. Note that \mathrm ~p can be different from the statement \neg p of the
logical negation In logic, negation, also called the logical complement, is an operation that takes a proposition P to another proposition "not P", written \neg P, \mathord P or \overline. It is interpreted intuitively as being true when P is false, and false ...
of ~p, depending on the completeness of the inference algorithm and thus also on the formal logic system. Negation as failure has been an important feature of logic programming since the earliest days of both
Planner Planner may refer to: * A personal organizer (book) for planning * Microsoft Planner * Planner programming language * Planner (PIM for Emacs) * Urban planner * Route planner * Meeting and convention planner * Japanese term for video game designer ...
and
Prolog Prolog is a 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 intended primarily ...
. In Prolog, it is usually implemented using Prolog's extralogical constructs. More generally, this kind of negation is known as weak negation, in contrast with the strong (i.e. explicit, provable) negation.


Planner semantics

In Planner, negation as failure could be implemented as follows: :''if'' (''not'' (''goal'' p)), ''then'' (''assert'' ¬p) which says that if an exhaustive search to prove p fails, then assert ¬p. This states that proposition p shall be assumed as "not true" in any subsequent processing. However, Planner not being based on a logical model, a logical interpretation of the preceding remains obscure.


Prolog semantics

In pure Prolog, NAF literals of the form \mathrm~p can occur in the body of clauses and can be used to derive other NAF literals. For example, given only the four clauses : p \leftarrow q \land \mathrm~r : q \leftarrow s : q \leftarrow t : t \leftarrow NAF derives \mathrm~s, \mathrm~r and ~p as well as ~t and ~q.


Completion semantics

The semantics of NAF remained an open issue until 1978, when Keith Clark showed that it is correct with respect to the completion of the logic program, where, loosely speaking, "only" and \leftarrow are interpreted as "if and only if", written as "iff" or "\equiv". For example, the completion of the four clauses above is : p \equiv q \land \mathrm~r : q \equiv s \lor t : t \equiv \mathrm : r \equiv \mathrm : s \equiv \mathrm 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 formula In mathematical logic, an atomic formula (also known as an atom or a prime formula) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformu ...
e. For example, to show \mathrm~p, NAF simulates reasoning with the equivalences : \mathrm~p \equiv \mathrm~q \lor r : \mathrm~q \equiv \mathrm~s \land \mathrm~t : \mathrm~t \equiv \mathrm : \mathrm~r \equiv \mathrm : \mathrm~s \equiv \mathrm In the non-propositional case, the completion needs to be augmented with equality axioms, to formalize the assumption that individuals with distinct names are distinct. NAF simulates this by failure of unification. For example, given only the two clauses : p(a) \leftarrow : p(b) \leftarrow t NAF derives \mathrm~p(c). The completion of the program is : p(X) \equiv X=a \lor X=b augmented with unique names axioms and domain closure axioms. The completion semantics is closely related both to
circumscription Circumscription may refer to: *Circumscribed circle *Circumscription (logic) *Circumscription (taxonomy) * Circumscription theory, a theory about the origins of the political state in the history of human evolution proposed by the American anthrop ...
and to the
closed world assumption The closed-world assumption (CWA), in a formal system of logic used for knowledge representation, is the presumption that a statement that is true is also known to be true. Therefore, conversely, what is not currently known to be true, is false. Th ...
.


Autoepistemic semantics

The completion semantics justifies interpreting the result \mathrm~p of a NAF inference as the classical negation \neg p of p. However, in 1987,
Michael Gelfond Michael Gelfond is a Professor in Computer Sciences at Texas Tech University in the United States. He received a degree in mathematics from the Steklov Institute of Mathematics in Russia in 1974 and emigrated to the United States in 1978. Gelfond's ...
showed that it is also possible to interpret \mathrm~p literally as "p can not be shown", "p is not known" or "p is not believed", as in autoepistemic logic. The autoepistemic interpretation was developed further by Gelfond and
Lifschitz Lifshitz (or Lifschitz) is a surname, which may be derived from the Polish city of Głubczyce (German: Leobschütz). The surname has many variants, including: , , Lifshits, Lifshuts, Lefschetz; Lipschitz (Lipshitz), Lipshits, Lipchitz, Lipschutz ( ...
in 1988, and is the basis of
answer set programming Answer set programming (ASP) is a form of declarative programming oriented towards difficult (primarily NP-hard) search problems. It is based on the stable model (answer set) semantics of logic programming. In ASP, search problems are reduced ...
. 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 A stable is a building in which livestock, especially horses, are kept. It most commonly means a building that is divided into separate stalls for individual animals and livestock. There are many different types of stables in use today; the ...
in the sense that : Δ = In other words, a set of assumptions Δ about what can not be shown is
stable A stable is a building in which livestock, especially horses, are kept. It most commonly means a building that is divided into separate stalls for individual animals and livestock. There are many different types of stables in use today; the ...
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, : p \leftarrow \mathrm~p has no stable expansions. : p \leftarrow \mathrm~q has exactly one stable expansion Δ = : p \leftarrow \mathrm~q : q \leftarrow \mathrm~p has exactly two stable expansions Δ1 = and Δ2 = . The autoepistemic interpretation of NAF can be combined with classical negation, as in extended logic programming and
answer set programming Answer set programming (ASP) is a form of declarative programming oriented towards difficult (primarily NP-hard) search problems. It is based on the stable model (answer set) semantics of logic programming. In ASP, search problems are reduced ...
. Combining the two negations, it is possible to express, for example : \neg p \leftarrow \mathrm~p (the closed world assumption) and : p \leftarrow \mathrm~\neg p (p holds by default).


Footnotes


References

* * * * * {{refend


External links


Report
from the W3C Workshop on Rule Languages for Interoperability. Includes notes on NAF and SNAF (scoped negation as failure). Logic programming Rules of inference