The object of this project is to develop the theory and applications of rewriting. The Knuth-Bendix completion procedure was originally intended as a means of taking an axiomatization of an equational theory and generating a rewrite system that can be used to decide whether a given equation follows from the others. Completion may also be used as a theorem-prover when it generates an infinite rewrite system. This work will extend the inference-rule and proof- normalization approach developed for completion to the generation of condition rewrite systems and to theorem proving in predicate calculus with equality. On the more practical side, the semantics of conditional rewriting will be explored as it applies to the functional and logic programming paradigms, and useful techniques for verifying aspects of program correctness will be developed.
