Tim@CIS.UPENN.EDU (Tim Finin) (11/21/86)
CIS COLLOQUIUM
University of Pennsylvania
3pm November 15, 1986
216 Moore School
COMPUTATIONAL PROBLEMS IN EQUATIONAL THEOREM PROVING
Dr. Paliath Narendran
General Electric Research Laboratory
The area of Equational Reasoning has recently gained a lot of attention
and has been found to have applications in such diverse areas as program
synthesis and data base queries. Most of these applications are centered
around using the equations as "rewrite rules" and, in particular, using
the Knuth-Bendix completion procedure to generate a "complete" set of
such rewrite rules. The power of the completion procedure lies in the
fact that once a complete set of rewrite rules is obtained, we also have
a decision procedure for the equational theory. We discuss some of the
main computational problems involved in this area such as unification,
matching and sufficient-completeness testing and outline the decidability
and complexity results.