On solving the equality problem in theories defined by Horn clauses (Q1085152)

The Knuth-Bendix completion procedure for solving the equality problem in equational theories is adapted to nonequational theories defined by sets of Horn clauses. Completeness can be achieved by endowing the procedure with a weak axiomatization of Boolean calculus and the reflexivity axiom for equality. It is shown that the procedure can also be used for inductive proofs, i.e., for proving universally quantified formulas in the initial model defined by a set of Horn clauses. The relationships to some resolution and paramodulation methods are discussed, and experimental results are appended.