{"id":{"repo_id":"vt","oai_identifier":"oai:vtechworks.lib.vt.edu:10919/52096"},"canonical_url":"https://search.dev.ndltd.org/etd/vt/oai:vtechworks.lib.vt.edu:10919/52096","repository":{"repo_id":"vt","name":"Virginia Tech","base_url":"https://vtechworks.lib.vt.edu/oai/request"},"display":{"title":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Zheng, Bing"],"institution":"Virginia Polytechnic Institute and State University","degree_name":"Master of Science","degree_level":"masters","degree_discipline":"Computer Science","degree_department":"Computer Science","school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":1989,"date_issued":"1989","date_published":"1989","updated_at":"2026-07-22T22:19:01Z","subjects":[],"languages":["en_US"],"rights":["In Copyright"],"rights_urls":["http://rightsstatements.org/vocab/InC/1.0/"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10919/52096","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.department","label":"Department","values":["Computer Science"]},{"key":"dc:creator","label":"Author","values":["Zheng, Bing"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2015-05-08T19:38:53Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2015-05-08T19:38:53Z"]},{"key":"dc:date.issued","label":"Date","values":["1989"]},{"key":"dc:publisher","label":"Institution","values":["Virginia Polytechnic Institute and State University"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.dcmitype","label":"Dc Type Dcmitype","values":["Text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master of Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Virginia Polytechnic Institute and State University"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en_US"]},{"key":"dc:rights","label":"Dc Rights","values":["In Copyright"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://rightsstatements.org/vocab/InC/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/10919/52096"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["Master of Science"]},{"key":"dc:format.mimetype","label":"Dc Format Mimetype","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Incorporating equation solving into unification through stratified term rewriting"]}]}],"canonical_facts":{"dc:contributor.department":["Computer Science"],"dc:creator":["Zheng, Bing"],"dc:date.accessioned":["2015-05-08T19:38:53Z"],"dc:date.available":["2015-05-08T19:38:53Z"],"dc:date.issued":["1989"],"dc:description.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."],"dc:description.degree":["Master of Science"],"dc:format.mimetype":["application/pdf"],"dc:identifier.uri":["http://hdl.handle.net/10919/52096"],"dc:language.iso":["en_US"],"dc:publisher":["Virginia Polytechnic Institute and State University"],"dc:rights":["In Copyright"],"dc:rights.uri":["http://rightsstatements.org/vocab/InC/1.0/"],"dc:title":["Incorporating equation solving into unification through stratified term rewriting"],"dc:type":["Thesis"],"dc:type.dcmitype":["Text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["masters"],"thesis:degree_name":["Master of Science"],"thesis:institution_name":["Virginia Polytechnic Institute and State University"]},"updated_at":"2026-07-22T22:19:01Z"}