Chase procedures are well-known decision and semi-decision procedures for the implication problem among dependencies, a speci fic type of first-order logic formulas, that are used for expressing database constraints. Of course, the implication problem can also be treated by general refutationally complete inference systems, like resolution with paramodulation. Recently the inference rule of basic paramodulation has been introduced and investigated as a strategy for exploring the search space for a refutation most ef ficiently. This paper demonstrates that chase procedures can be seen as special instances of basic paramodulation by de fining the parameters of basic paramodulation, a reduction ordering and a term selection function, appropriately. The mutual simulation of chase procedures and basic paramodulation also extends to the completeness proofs.
Author and article information
Fachbereich Informatik, Universität Dortmund
D-44221 Dortmund, Germany