
Chapter
1
:
Negation in Logic Programming
Negation
as
Failure
By "negation as failure" or SLDNF-resolution, we mean the result of adding
negation as failure to SLD-resolution, i.e., the query evaluation procedure
described in Clark [1978], where a negative literal is selected only if it is a
ground literal —iA. The next step is then to query A; if A succeeds, then the
evaluation of —iA fails; if A fails on every evaluation path then, —iA suc-
ceeds. Since by König's lemma the evaluation tree is then finite, this is usually
called finite failure to distinguish it from the situation where the evaluation tree
has no successful path but has infinit ...