Efficient deduction in equality Horn logic by Horn-completion

Abstract

We present a new unfailing completion procedure for Horn clauses with equality, including goal clauses. It is refutationally complete, and improves previous methods in that superpositions are computed only with unconditional equations, and on one single arbitrarily chosen equation in the condition of each Horn axiom, (i.e. not necessarily on the maximal ones). An interesting aspect of this note is the proof of completeness, which is based on the techniques defined by Bachmair and Ganzinger (1990). It is given here in detail and is short, simple and highly self-contained.