High performance simplification-based automated deduction

Equational logic is one of the most important domains of research in computer science. Therefore, automated deduction in equational logic an important subject of research. However, the seemingly insurmountable search space caused by the symmetry and replacement properties of the equality predicate had been a serious obstacle which baffled researchers in automated deduction for several decades. It is not until very recently that methods capable of effectively reason with equations have been designed and successfully applied to an interesting range of challenging problems. These methods are based on the term rewriting approach to equational reasoning. The key idea in term rewriting based theorem proving is to regard a derivation as a process of proof reduction. Equations are oriented into rules according to a well-founded ordering, and equational replacement is performed only in one direction. By keeping every piece of data fully simplified at all time, the search space is drastically reduced.