Equational Theorem Proving and Rewrite Rule Systems

Equational theorem proving is interesting both from a mathematical and a computational point of view. Many mathematical structures like monoids, groups, etc. can be described by equational axioms. So the theory of free monoids, free groups, etc. is the equational theory defined by these axioms. A decision procedure for the equational theory is a solution for the word problem over the associated algebraic structure. From a computational point of view, abstract data types are basically described by equations. Thus, proving properties of an abstract data type amounts to proving theorems in the associated equational theory.One approach to equational theorem proving consists in associating a direction with the equational axioms, thus transforming them into rewrite rules. Now in order to prove an equation a = b, the rewrite rules are applied to both sides, finally yielding reduced versions a’ and b’ of the left and right hand sides, respectively. If a’ and b’ agree syntactically, then the equation holds in the equational theory. However, in general this argument cannot be reversed; a’ and b’ might be different even if a = b is a theorem. The reason for this problem is that the rewrite system might not have the Church-Rosser property. So the goal is to take the original rewrite system and transform it into an equivalent one which has the desired Church-Rosser property.We show how rewrite systems can be used for proving theorems in equational and inductive theories, and how an equational specification of a problem can be turned into a rewrite program.