Negation as failure

From Wikipedia, the free encyclopedia

Negation as failure is an interpretation of logical negation according to which the negation of a formula is true if and only if the formula cannot be proved true. Negation as failure is used in logic programming languages such as Prolog. Thus in Prolog the compiler holds that the absence of evidence equals evidence for absence.

In logic, the standard interpretation of negation is that the negation of a formula is true if and only if the formula is false. If a formula is neither true nor false, its negation is considered unknown. On the converse, the negation of the formula is considered true according to the interpretation of negation as failure.

The negation used in Prolog is treated as negation as failure by the interpreter. If, during the course of execution of a program, the interpreter has to evaluate NOT a(b), it tries to prove that a(b) is true. If this attempt is unsuccessful, NOT a(b) is considered true.

Negation as failure is related to the common default assumption that what is not known to be true is false. This is known as the Closed World Assumption.

In argumentation, a point for which no argument can be made is called the unfounded argument. An unfounded argument for α is not a founded argument for the negation of α.