Universal code (data compression): Difference between revisions

From formulasearchengine
Jump to navigation Jump to search
en>Addbot
m Bot: Migrating 3 interwiki links, now provided by Wikidata on d:q4176366
en>28bytes
m References: fix bare url
 
Line 1: Line 1:
'''Negation as failure''' ('''NAF''', for short) is a [[non-monotonic logic|non-monotonic]] inference rule in [[logic programming]], used to derive <math>\mathrm{not}~p</math> (i.e. that <math>~p</math> is assumed not to hold) from failure to derive <math>~p</math>.  Note that <math>\mathrm{not} ~p</math> can be different from the statement <math>\neg p</math> of the [[negation|logical negation]] of <math>~p</math>, depending on the completeness of the inference algorithm and thus also on the formal logic system.
.mw-body, mtext {
 
    font-family: Cambria;
Negation as failure has been an important feature of logic programming since the earliest days of both [[Planner (programming_language)|Planner]] and [[Prolog]]. In Prolog, it is usually implemented using Prolog's extralogical constructs.
}
 
math {
==Planner semantics==
    font-family: Cambria Math;
In Planner, negation as failure could be implemented as follows:
}
:<tt>''if'' (''not'' (''goal'' p)),  ''then'' (''assert'' ¬p) </tt>
which says that if the goal to prove <tt>p</tt> fails, then assert <tt>¬p</tt>.  Note that the above example uses true mathematical negation, which cannot be expressed in Prolog.
 
==Prolog semantics==
In pure Prolog, NAF literals of the form <math>not~p</math> can occur in the body of clauses and can be used to derive other NAF literals. For example, given only the four clauses
 
: <math>p \leftarrow q \and \mathrm{not}~r</math>
: <math>q \leftarrow s</math>
: <math>q \leftarrow t</math>
: <math>t \leftarrow</math>
 
NAF derives <math>\mathrm{not}~s</math>, <math>\mathrm{not}~r</math> and <math>~p</math>.
 
==Completion semantics==
 
The semantics of NAF remained an open issue until Keith Clark [1978] showed that it is correct with respect to the completion of the logic program, where, loosely speaking, "only" and <math>\leftarrow</math> are interpreted as "if and only if", written as "iff" or "<math>\equiv</math>".
 
For example, the completion of the four clauses above is
 
: <math>p \equiv q \and \mathrm{not}~r</math>
: <math>q \equiv s \or t</math>
: <math>t \equiv \mathrm{true}</math>
: <math>r \equiv \mathrm{false}</math>
: <math>s \equiv \mathrm{false}</math>
 
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]]e. For example, to show <math>\mathrm{not}~p</math>, NAF simulates reasoning with the equivalences
 
: <math>\mathrm{not}~p \equiv \mathrm{not}~q \or r</math>
: <math>\mathrm{not}~q \equiv \mathrm{not}~s \and \mathrm{not}~t</math>
: <math>\mathrm{not}~t \equiv \mathrm{false}</math>
: <math>\mathrm{not}~r \equiv \mathrm{true}</math>
: <math>\mathrm{not}~s \equiv \mathrm{true}</math>
 
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
 
: <math>p(a) \leftarrow</math>
: <math>p(b) \leftarrow</math> t
 
NAF derives <math>\mathrm{not}~p(c)</math>.
 
The completion of the program is
 
: <math>p(X) \equiv X=a \or X=b</math>
 
augmented with unique names axioms and domain closure axioms.
 
The completion semantics is closely related both to [[Circumscription (logic)|circumscription]] and to the [[closed world assumption]].
 
==Autoepistemic semantics==
 
The completion semantics justifies interpreting the result <math>\mathrm{not}~p</math> of a NAF inference as the classical negation <math>\neg p</math> of <math>p</math>. However, Michael Gelfond [1987] showed that it is also possible to interpret <math>\mathrm{not}~p</math> literally as "<math>p</math> can not be shown", "<math>p</math> is not known" or "<math>p</math> is not believed", as in [[autoepistemic logic]]. The autoepistemic interpretation was developed further by Gelfond and Lifschitz [1988] 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 model semantics|stable]] in the sense that 
 
: Δ = {<math>\mathrm{not}~p</math> | <math>p</math> is not implied by P  ∪  Δ}
 
In other words, a set of assumptions Δ about what can not be shown is [[Stable model semantics|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
 
: <math>p \leftarrow \mathrm{not}~p</math>
has no stable expansions.
 
: <math>p \leftarrow \mathrm{not}~q</math>
has exactly one stable expansion Δ = {<math>\mathrm{not}~q</math>}
 
: <math>p \leftarrow \mathrm{not}~q</math>
: <math>q \leftarrow \mathrm{not}~p</math>
has exactly two stable expansions  Δ<sub>1</sub> = {<math>\mathrm{not}~p</math>} and Δ<sub>2</sub> = {<math>\mathrm{not}~q</math>}.
 
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
 
: <math>\neg p \leftarrow \mathrm{not}~p</math> (the closed world assumption) and
: <math>p \leftarrow \mathrm{not}~\neg p</math> (<math>p</math> holds by default).
 
==References==
 
* K. Clark [1978, 1987]. [http://www.doc.ic.ac.uk/~klc/neg.html Negation as failure]. ''Readings in nonmonotonic reasoning'', Morgan Kaufmann Publishers, pages 311-325.
 
* M. Gelfond [1987] [http://www.cs.ttu.edu/~mgelfond/papers/autoepistemic.pdf On Stratified Autoepistemic Theories] Proc. AAAI, pages 207-211.
 
* M. Gelfond and V. Lifschitz [1988] [http://www.cs.ttu.edu/~mgelfond/papers/stable.pdf The Stable Model Semantics for Logic Programming] Proc.  5th International Conference and Symposium on Logic Programming (R. Kowalski and K. Bowen, eds), MIT Press, pages 1070-1080.
 
* J.C. Shepherdson [1984] ''Negation as failure: a comparison of Clark's completed data base and Reiter's closed world assumption'', Journal of Logic Programming, vol 1, 1984, pages 51-81.
 
* J.C. Shepherdson [1985] ''Negation as failure II'', Journal of Logic Programming, vol 3, 1985, pages 185-202.
 
==External links==
 
* [http://www.w3.org/2004/12/rules-ws/report/ Report] from the W3C Workshop on Rule Languages for Interoperability. Includes notes on NAF and SNAF (scoped negation as failure).
 
[[Category:Logic programming]]
[[Category:Rules of inference]]

Latest revision as of 21:34, 10 March 2014

.mw-body, mtext {
    font-family: Cambria;
}
math {
    font-family: Cambria Math;
}