Incorporating equation solving into unification through stratified term rewriting

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.

Name thesis:degree_name

Master of Science

Level thesis:degree_level

masters

Discipline thesis:degree_discipline

Computer Science

Department dc:contributor.department

Computer Science

Grantor dc:publisher

Virginia Polytechnic Institute and State University

Year dc:date.issued

1989

Author dc:creator

• Zheng, Bing

Statement dc:rights

• In Copyright

Licence dc:rights.uri

• http://rightsstatements.org/vocab/InC/1.0/

Language dc:language.iso

en_US

Handle dc:identifier.uri

http://hdl.handle.net/10919/52096

OAI identifier oai:identifier

oai:vtechworks.lib.vt.edu:10919/52096