4 Building-in Equational Theories G. D. Plotkin

INTRODUCTION If let loose, resolution theorem-provers can waste time in many ways. They can continually rearrange the multiplication brackets of an associative multiplication operation or replace terms t by ones like f(f(f(t, e), e), e) where f is a multiplication function and e is its identity. Generally they continually discover and misapply trivial lemmas. Global heuristics using term complexity do not help much and ad hoc devices seem suspicious. On the other hand, one would like to evaluate terms when possible, for example we would want to replace 5 4 by 9. More generally one would like to have liberty to simplify, to factorise and to rearrange terms. The obvious way to deal with an associative multiplication would be to imitate people, and just drop the multiplication brackets. However used or abused the basic facts involved in such manipulations form an equational theory, T, that is, a theory all of whose sentences are universal closures of equations. Under certain conditions, we will be able to build the equational theory into the rules of inference. The resulting method will be resolution-like, the difference being that concepts are defined using provable equality between terms rather than literal identity. Therefore the set of clauses expressing the theory will not be among the input clauses, so no time will be wasted in the misapplication of trivial lemmas, since the rules will not waste time in this way.