
Chapter 9: Database Integrity 361
dure in these cases can be implemented with efficiencies comparable to that of
Prolog implementations, as described in Kowalski, Sadri, and Soper [1987].
We have not yet proved the analogue of Theorem 5 for the general case.
The main difficulty comes from the need to generalize the and-tree in the proof
of Theorem 4 to a tree including auxiliary proofs of negation as failure. These
auxiliary proofs are not simple and-trees but include entire finitely failed search
spaces. This suggests that we may be able to deal with this case by converting
finitely failed search spaces into direct proofs of negative condition ...