On solving the equality problem in theories defined by Horn clauses

Abstract

We propose in this paper a slight modification of the Knuth and Bendix algorithm for solving the equality problem in non-equational theories defined by a set of Horn clauses. We prove that the completeness property of the algorithm is then preserved, provided that a weak axiomatization of boolean calculus and equality has been given to the algorithm. In particular, we need only the reflexivity axiom for equality. This algorithm can also be interpreted as the extension to Horn clauses of the resolution/narrowing algorithm proposed by Lankford [LA], which applies only when the equality predicate does not occur positively in non-unit clauses. We give some examples of theorems proved by this method, which show its efficiency in comparison with other paramodulation-based methods. Another application of the Knuth and Bendix algorithm is the proof by induction (Musser [MU], Huet-Hullot [HH], and others). We show that our version of the completion algorithm can be used for proving universally quantified formulas (not only equations) in the initial model defined by a set of Horn clauses.