What is Failure?   An Approach to Constructive Negation
W{\l}odzimierz Drabent
Acta Informatica, 32(1):27-59, February 1995

Abstract:

A standard approach to negation in logic programming is negation as
failure.  Its major drawback is that it cannot produce answer
substitutions to negated queries.  Approaches to overcoming this
limitation are termed constructive negation.  This work proposes an
approach based on construction of {\em failed trees} for some
instances of a negated query.  For this purpose a generalization of
the standard notion of a failed tree is needed.  We show that a
straightforward generalization leads to unsoundness and present a
correct one.

The method is applicable to arbitrary normal programs.  If finitely
failed trees are concerned then its semantics is given by Clark
completion in 3-valued logic (and our approach is a proper extension
of SLDNF-resolution).  If infinite failed trees are allowed then we
obtain a method for the well-founded semantics.  In both cases
soundness and completeness are proved.