An Equality Theorem Prover Based on Grammar Rewriting

We present the implementation of a term rewriting procedure based on congruence closure. The procedure can be used with arbitrary equational theories. It uses context free grammars to represent equivalence classes of terms. This representation is moti-vated by the need to handle equational theories where confluence cannot be achieved un-der traditional term rewriting. Context free grammars provide concise representation of arbitrary-sized equivalence classes of terms. In some equational theories where confluence cannot be achieved under term rewriting, it can be achieved under grammar rewriting, where the whole equivalence class of terms is ultimately represented with one context free grammar. Also, grammar rewriting can be used in any equational theory, besides the ones that have no confluent term rewriting system, to give an alternative form of rewriting. In the implementation of the procedure, we are concerned with the practical issue of how to build an efficient equality theorem prover using grammar rewriting. This involves representing the system in a clear and efficient way in the language C++. Also it involves constructing, and expreimenting with heuristics on the ordering of the queu