@inproceedings{DBLP:conf/vldb/KowalskiSS87, author = {Robert A. Kowalski and Fariba Sadri and Paul Soper}, editor = {Peter M. Stocker and William Kent and Peter Hammersley}, title = {Integrity Checking in Deductive Databases}, booktitle = {VLDB'87, Proceedings of 13th International Conference on Very Large Data Bases, September 1-4, 1987, Brighton, England}, publisher = {Morgan Kaufmann}, year = {1987}, isbn = {0-934613-46-X}, pages = {61-69}, ee = {db/conf/vldb/KowalskiSS87.html}, crossref = {DBLP:conf/vldb/87}, bibsource = {DBLP, http://dblp.uni-trier.de} }
We describe the theory and implementation of a general theorem-proving technique for checking integrity of deductive databases recently proposed by Sadri and Kowalski. The method uses an extension of the SLDNF proof procedure and achieves the effect of the simplification algorithms of Nicolas, Lloyd, Topor et al, and Decker by reasoning forwards from the update and thus focusing on the relevant parts of the database and the relevant constraints.
Formalisation of the procedure using logic as metalanguage forms the basis of our implementation in Prolog. It is further shown that in the absence of implicit deletions a transformation of the database clauses and constraints allows the method to be implemented with efficiencies comparable to implementations of Prolog.
Copyright © 1987 by the VLDB Endowment. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the VLDB copyright notice and the title of the publication and its date appear, and notice is given that copying is by the permission of the Very Large Data Base Endowment. To copy otherwise, or to republish, requires a fee and/or special permission from the Endowment.