Proof methods for equational theories
Leo Bachmair · 1987
In this thesis we study the application of rewrite techniques to equational reasoning. We present various rewrite-based proof methods and formalize them on an abstract level as equational inference systems. We also introduce techniques, based on the concept of proof orderings, for reasoning about such inference systems. We describe the standard Knuth-Bendix completion method in our formalism and establish its correctness. Our correctness proofs are comparatively simple and apply to a large class of specific versions of completion. The notion of critical pair criterion can also be conveniently formalized in our framework. We further discuss completion for rewriting modulo a congruence and present methods that are more general in scope than other completion procedures. We present, for instance, a completion procedure that can be applied to equational theories with infinite congruence classes; a case that can not be handled by any other method. We also describe an extension of standard completion, completion without failure, that often succeeds in constructing a canonical system when standard completion fails. Unfailing completion is also a refutationally complete theorem prove for purely equational theories. Finally, we describe some techniques for providing the termination of rewrite systems.