{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/20259"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/20259","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Semantic unification for convergent systems","abstract":"Equation solving is the process of finding a substitution of terms for variables that makes two terms equal in a given theory, while semantic unification is the process that generates a basis set of such unifying substitutions. A simpler variant of the problem is semantic matching, where the substitution is made in only one of the terms. Semantic unification and matching constitute an important component of theorem proving and programming language interpreters.","abstract_html":"Equation solving is the process of finding a substitution of terms for variables that makes two terms equal in a given theory, while semantic unification is the process that generates a basis set of such unifying substitutions. A simpler variant of the problem is semantic matching, where the substitution is made in only one of the terms. Semantic unification and matching constitute an important component of theorem proving and programming language interpreters.","abstract_has_math":false,"creators":["Mitra, Subrata"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Dershowitz, Nachum"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-05-07T12:33:58Z","date_published":"2011-05-07T12:33:58Z","updated_at":"2026-07-22T22:25:15Z","subjects":["Computer Science"],"languages":["eng"],"rights":["Copyright 1994 Mitra, Subrata"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI9512489","(UMI)AAI9512489"],"render_values":[{"text":"AAI9512489","href":null,"code":true},{"text":"(UMI)AAI9512489","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2142/20259","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Dershowitz, Nachum"]},{"key":"dc:creator","label":"Author","values":["Mitra, Subrata"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-05-07T12:33:58Z","10000-01-01","1994"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 1994 Mitra, Subrata"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI9512489","(UMI)AAI9512489","http://hdl.handle.net/2142/20259"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Equation solving is the process of finding a substitution of terms for variables that makes two terms equal in a given theory, while semantic unification is the process that generates a basis set of such unifying substitutions. A simpler variant of the problem is semantic matching, where the substitution is made in only one of the terms. Semantic unification and matching constitute an important component of theorem proving and programming language interpreters.","In this thesis we formulate a unification procedure based on a system of transformation rules that looks at goals in a lazy, top-down fashion, and prove its soundness and completeness for equational theories described by convergent rewrite systems (finite sets of equations that compute unique output values when applied from left-to-right to input values).","We consider different variants of the system of transformation rules. We describe syntactic restrictions on the equations under which simpler sets of transformation rules are sufficient for generating a complete set of semantic matchings. We show that our first-order unification procedure, with slight modifications, can be used to solve the satisfiability problem in combinatory logic together with a convergent set of algebraic axioms, resulting in a complete higher-order unification procedure for the given algebra. We also provide transformation rules to handle situations where some of the function symbols additionally satisfy the equivalences of associativity and commutativity.","\"Termination of a system of directed equations is essential for proving existence and uniqueness of normal forms. Furthermore, termination is essential for simplification in theorem provers. We provide a simple restriction on the well-known \"\"recursive path ordering\"\" which can be used for proving termination of extended rewriting, modulo the axioms of associativity and commutativity.\"","Finally, we formulate various syntactic and semantic conditions on the given equations and the goal which result in decidability of semantic matching. We also investigate decidable cases of semantic unification.","Made available in DSpace on 2011-05-07T12:33:58Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 9512489.pdf: 5489758 bytes, checksum: aeb80964d8e83a7497957420b05e490c (MD5) Previous issue date: 1994","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T14:42:42Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:18:35-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission","ETDs are only available to UIUC Users without author permission","U of I Only"]},{"key":"dc:title","label":"Title","values":["Semantic unification for convergent systems"]}]}],"canonical_facts":{"dc:contributor":["Dershowitz, Nachum"],"dc:creator":["Mitra, Subrata"],"dc:date":["2011-05-07T12:33:58Z","10000-01-01","1994"],"dc:description":["Equation solving is the process of finding a substitution of terms for variables that makes two terms equal in a given theory, while semantic unification is the process that generates a basis set of such unifying substitutions. A simpler variant of the problem is semantic matching, where the substitution is made in only one of the terms. Semantic unification and matching constitute an important component of theorem proving and programming language interpreters.","In this thesis we formulate a unification procedure based on a system of transformation rules that looks at goals in a lazy, top-down fashion, and prove its soundness and completeness for equational theories described by convergent rewrite systems (finite sets of equations that compute unique output values when applied from left-to-right to input values).","We consider different variants of the system of transformation rules. We describe syntactic restrictions on the equations under which simpler sets of transformation rules are sufficient for generating a complete set of semantic matchings. We show that our first-order unification procedure, with slight modifications, can be used to solve the satisfiability problem in combinatory logic together with a convergent set of algebraic axioms, resulting in a complete higher-order unification procedure for the given algebra. We also provide transformation rules to handle situations where some of the function symbols additionally satisfy the equivalences of associativity and commutativity.","\"Termination of a system of directed equations is essential for proving existence and uniqueness of normal forms. Furthermore, termination is essential for simplification in theorem provers. We provide a simple restriction on the well-known \"\"recursive path ordering\"\" which can be used for proving termination of extended rewriting, modulo the axioms of associativity and commutativity.\"","Finally, we formulate various syntactic and semantic conditions on the given equations and the goal which result in decidability of semantic matching. We also investigate decidable cases of semantic unification.","Made available in DSpace on 2011-05-07T12:33:58Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 9512489.pdf: 5489758 bytes, checksum: aeb80964d8e83a7497957420b05e490c (MD5) Previous issue date: 1994","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T14:42:42Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:18:35-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission","ETDs are only available to UIUC Users without author permission","U of I Only"],"dc:identifier":["AAI9512489","(UMI)AAI9512489","http://hdl.handle.net/2142/20259"],"dc:language":["eng"],"dc:rights":["Copyright 1994 Mitra, Subrata"],"dc:subject":["Computer Science"],"dc:title":["Semantic unification for convergent systems"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:15Z"}