[Prev][Next][Index][Thread]

[rmb%bu-cs.bu.edu@bu-it.BU.EDU: BU colloq announcements]



Return-Path: <rmb@bu-cs.bu.edu>
Date: Thu, 18 Feb 88 17:25:46 EST
From: rmb%bu-cs.bu.edu@bu-it.BU.EDU
To: colloq@bu-cs.bu.edu
Subject: BU colloq announcements


			COMPUTER SCIENCE DEPARTMENT
			  College of Liberal Arts
		      111 Cummington Street, room 138
		        Boston, Massachusetts, 02215
			 telephone (617) 353-8919

Date:		Wednesday, February 24, 1988
Time:		10:00 a.m.  (tea at 9:45)
Place:		Room 135 at 111 Cummington Street
Speaker:	Wayne Snyder,
		Department of Computer and Information Science 
		University of Pennsylvania		
Title:		COMPLETE SETS OF TRANSFORMATIONS	
		FOR GENERAL $E$-UNIFICATION

Abstract:
    E-unification is a generalization of unification which permits the
use of equality in theorem proving and logic programming.  Many
special algorithms have been developed in the last decade for special
theories, such as associativity and commutativity, but to date the
problem of unifying terms in the presence of an arbitrary set of
equations been little studied.
   In this talk we present a procedure which is sound and complete for
any theory E, based on the abstract method of transformations on
systems of terms used by Martelli-Montanari to study standard
unification.  The completeness proof uses a simple version of the
notion of the completion of a set of equations (as in the Knuth-Bendix
procedure), and shows exactly what restrictions we can place on the
general method without sacrificing completeness. Several interesting
issues, such as the problem of proving the completeness of methods
which perform `eager variable elimination,' are highlighted by this
abstract approach.