# The ICICS/CS Reading Room

## UBC CS TR-86-09 Summary

- No on-line copy of this technical report is available.

- Precomplete Negation \& Universal Quantification, April 1986 Paul J. Voda
This paper is concerned with negation in logic programs. We propose to
extend negation as failure by a stronger form of negation called precomplete
negation. In contrast to negation as failure, precomplete negation has a simple
semantic characterization given in terms of computational theories which deliberately abandon the law of the excluded middle (and thus classical negation) in
order to attain computational efficiency. The computation with precomplete
negation proceeds with the direct computation of negated formulas even in the
presence of free variables. Negated formulas are computed in a mode which is
dual to the standard positive mode of logic computations. With negation as
failure the formulas with tree variables must be delayed until the latter obtain
values. Consequently, in situations where delayed formulas are never sufficiently
instantiated, precomplete negation can find solutions unattainable with negation
as failure. As a consequence of delaying, negation as failure cannot compute
unbounded universal quantifiers whereas precomplete negation can. Instead of
concentrating on the model-theoretical side of precomplete negation this paper
deals with questions of complete computations and efficient implementations.

If you have any questions or comments regarding this page please send mail to
help@cs.ubc.ca.