[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.