Equational Reasoning in Saturation-Based Theorem Proving
Leo Bachmair, Harald Ganzinger · 1998
INTRODUCTION Equational reasoning is fundamental in mathematics, logics, and many applications of formal methods in computer science. In this chapter we describe the theoretical concepts and results that form the basis of state-of-the-art automated theorem provers for first-order clause logic with equality. We mainly concentrate on refinements of paramodulation, such as the superposition calculus, that have yielded the most promising results to date in automated equational reasoning. We begin with some preliminary material in section 2 and then explain, in section 3, why resolution with the congruence axioms is an impractical theorem proving method for equational logic. In section 4 we outline the main results about paramodulation---a more direct equational inference rule. This section also contains a description of the modification method, which can be used to demonstrate that the functional reflexivity axioms are redundant in the context of paramodulation. The modification