Incorporating equation solving into unification through stratified term rewriting

Abstract

This thesis studies equational theories incorporated into unification and describes STAR, a stratified term rewriting system that achieves a full integration. STAR is an advance over existing systems because it integrates an equational theory with unification at a lower, more fundamental level. Certain properties of STAR are proven including termination and confluence.

We also discuss the algorithmic complexity of the reduction algorithm, a vital component of STAR. We compare our system with narrowing and discuss the merits and drawbacks of each technique.

Since our system is an experimental integration of equation solving and unification, we are not concerned with the efficiency of the implementation. We do propose, however, some future improvements.