Files in this item



application/pdf9512489.pdf (5MB)Restricted to U of Illinois
(no description provided)PDF


Title:Semantic unification for convergent systems
Author(s):Mitra, Subrata
Doctoral Committee Chair(s):Dershowitz, Nachum
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Computer Science
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.
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.
Issue Date:1994
Rights Information:Copyright 1994 Mitra, Subrata
Date Available in IDEALS:2011-05-07
Identifier in Online Catalog:AAI9512489
OCLC Identifier:(UMI)AAI9512489

This item appears in the following Collection(s)

Item Statistics