A slick procedure for integrity checking in deductive databases

We present a resolution-based proof procedure called SLIC, for integrity checking in deductive databases. Sadri and Kowalski's meta-level rules are replaced in SLIC by much simpler inference steps. sue optimizes the tradeoff between focusing the evaluation of integrity constraints on the difference of consecutive database states, on one hand, and the cost of generating that difference with sufficient precision, on the other sue is sound. It is complete in each case for which also SLDNF is complete. sue terminates in a large class of cases. We present a sufficient condition for ensuring the termination of SLIe and also SLDNF, by generalizing the class of acyclic databases and bounded queries.