Precomplete Negation & Universal Quantification

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.