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. / Master of Science
| Identifer | oai:union.ndltd.org:VTETD/oai:vtechworks.lib.vt.edu:10919/52096 |
| Date | January 1989 |
| Creators | Zheng, Bing |
| Contributors | Computer Science |
| Publisher | Virginia Polytechnic Institute and State University |
| Source Sets | Virginia Tech Theses and Dissertation |
| Language | en_US |
| Detected Language | English |
| Type | Thesis, Text |
| Format | vi, 74 leaves, application/pdf, application/pdf |
| Rights | In Copyright, http://rightsstatements.org/vocab/InC/1.0/ |
| Relation | OCLC# 20305522 |
Page generated in 0.0024 seconds