×

Extending SLD resolution to equational Horn clauses using E-unification. (English) Zbl 0668.68111

We study the role of unification modulo a set of equations, or E- unification, in the context of refutation methods for sets of Horn clauses with equality. Two extensions of SLD resolution based on E- unification are presented, and rigorous completeness results are shown, including an analysis of the ground case for insight into the computational implications. The concept of a congruence closure generalized to sets of ground Horn clauses is central to these completeness results. The first method is general, in that it applies to arbitrary sets of equational Horn clauses, but is not practical, as it assumes a procedure which gives an explicit sequence of substitutions for each E-unifier. A second method uses a procedure enumerating a complete set of E-unifiers, and appears to be well suited to a class of “well- behaved” equational logic programs which allows a clean and natural integration of the functional and logic-programming paradigms. Using this second method, we have formalized the refutation method used in Eqlog for this class of programs, and a theorem establishes rigorously the completeness of this method. We compare these methods in detail with related work, and show that other methods either explicitly include E- unification or simulate it in some manner.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
PDFBibTeX XMLCite
Full Text: DOI