Completion Without Failure
Leo Bachmair, Nachum Dershowitz, David A. Plaisted · 1989
. We present an "unfailing" extension of the standard KnuthBendix completion procedure that is guaranteed to produce a desired canonical system, provided certain conditions are met. We prove that this unfailing completion method is refutationally complete for theorem proving in equational theories. The method can also be applied to Horn clauses with equality, in which case it corresponds to positive unit resolution plus oriented paramodulation, with unrestricted simplification. 1 This research was supported in part by the National Science Foundation under grants DCR 85-13417 and DCR 85-16243. 1 Introduction The design of efficient methods for dealing with the equality predicate is one of the major goals in automated theorem proving. Just adding equality axioms almost invariably leads to unacceptable inefficiencies. Instead, a number of special methods have been devised for reasoning about equality. Within resolution-based provers, demodulation, that is, using equations in only one ...