Relational Chase Procedures Interpreted as Resolution with Paramodulation¹

Article type: Research Article

Authors: Biskup, Joachim^a | Convent, Bernhard^b

Affiliations: [a] Department of Computer Science, University of Hildesheim, Marienburger Platz 22, D-3200 Hildesheim, Germany | [b] IBM Scientific Center Heidelberg, Tiergartenstr. 15, D-6900 Heidelberg, Germany

Note: [1] Research was done while this author was with the University of Hildesheim.

Abstract: In this paper the relationship between dependency theory and first-order logic is explored in order to show how relational chase procedures (i.e., algorithms to decide inference problems for dependencies) can be interpreted as clever implementations of well known refutation procedures of first-order logic with resolution and paramodulation. On the one hand this alternative interpretation provides a deeper insight into the theoretical foundations of chase procedures, whereas on the other hand it makes available an already well established theory with a great amount of known results and techniques to be used for further investigations of the inference problem for dependencies. Our presentation is a detailed and careful elaboration of an idea formerly outlined by Grant and Jacobs which up to now seems to be disregarded by the database community although it definitely deserves more attention.

DOI: 10.3233/FI-1991-15203

Journal: Fundamenta Informaticae, vol. 15, no. 2, pp. 123-138, 1991