On solving the equality problem in theories defined by Horn clauses

AbstractIn this paper we propose a slight modification of the Knuth and Bendix completion procedure for solving the equality problem in nonequational theories defined by a set of Horn clauses. We prove that the completeness property of this procedure is then preserved, provided that a weak axiomatization of boolean calculus and equality has been given to the procedure. In particular, we need only the reflexivity axiom for equality.Another application of the Knuth and Bendix procedure is the proof by induction (Musser, 1980; Huet-Hullot, 1982 and others). We show that our version of the completion procedure can be used for proving universally quantified formulas (not only equations) in the initial model defined by a set of Horn clauses.Experimental results, and comparisons with other resolution/paramodulation-based methods, in particular the methods proposed by Lankford (1975) and Peterson (1983), are included in the paper