tim@LINC.CIS.UPENN.EDU.UUCP (04/29/87)
PhD Dissertation Proposal
General E-Unification:
Complete Transformations for Equational
Theorem Proving and Logic Programming
Wayne Snyder
Computer and Information Science
University of Pennsylvania
There has been much work in the past two decades on the problem of
incorporating methods for equational reasoning into computational
logic. Unfortunately, the ``substitution of equals for equals'' which
forms the basis of equational reasoning is fundamentally different
from the analytic methods used for non-equational reasoning, which are based
on an interpretation of the connectives in the language. This dicotomy
has convinced many researchers that we should stratify theorem provers
into a (non-equational) refutation mechanism and an E-unification
mechanism which performs equational reasoning during unification steps,
so that two terms E-unify if they are unifiable modulo the congruence
on terms induced by the set of equations E. Many special purpose E-unification
procedures have been designed for particular equational theories, and
several also for the class of theories which can be compiled into
rewrite rules via the Knuth-Bendix procedure. So far the problem
of E-unification for arbitrary equational theories has received little
attention, and in general there seems to be a need for some integrated
approach which will show the structure of the class of all
E-unification problems.
Our current research attempts to address the problem of general
E-unification and higher-order unification by extending the method
of transformations on term systems, developed in the context of
standard unification by Martelli and Montanari. We hope that this
approach will provide not only a basis for practical procedures, but
also a means for analysing unification problems in an abstract and
mathematically elegant fashion. Our results so far include a completeness
proof for our procedure and a new analysis of the occur check problem
in E-unification. We propose to extend these methods to refutation
methods incorporating equality, to a fundamentally new form of
E-unification which has come up in the study of equational matings,
and to the problem of higher-order E-unification. It is our hope that
this research will not only yield interesting theoretical results,
but will also help us to find practical algorithms for theorem proving
and logic programming in the presence of equality.
Friday, May 1, 10:00am
556 Moore (Conference Room)
Supervisor: Dr. Jean Gallier
Committee: Dr. Dale Miller (Chairman)
Dr. Peter Buneman
Dr. Frank Pfenning (CMU)
Dr. Paliath Narendran (GE)
Dr. Andre Scedrov