Negation by constraints: a sound and efficient implementation of negation in deductive databases

Negation is investigated in the context of deductive databases which can be viewed as function-free logic programs. An improved form of negation from the program completion is introduced in which a sound computation rule can select for evaluation negative goals containing free variables. This means that programs never flounder. The procedural semantics of this negation, termed negation by constraints, requires the introduction of negated goals with existentially and universally quantified variables. While providing many of the advantages of evaluation by saturation, its implementation is comparable in efficiency with the implementation of negation by failure.