A PROGRAM FOR GENERATING AND ANALYZING TERM REWRITING SYSTEMS
Randy Forgaard · DSpace@MIT (Massachusetts Institute of Technology) · 1984
This thesis presents new results in the use of term rewriting systems for automatic theorem proving. The design and implementation of REVE 2, a computer program that incorporates these results, is described. In addition, an introduction to the basic theory, procedures, and algorithms of term rewriting is provided, in a manner suitable for non-specialists.