Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-92-247

Difference unification

Basin, David A. and Walsh, Toby

MPI-I-92-247. November 1992, 15 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
We extend previous work on difference identification and reduction
as a technique for automated reasoning. We generalize unification so
that terms are made equal not only by finding substitutions for
variables but also by hiding term structure. This annotation of
structural differences
serves to direct rippling, a kind of rewriting designed to
remove structural differences in a controlled way. On the
technical side, we give a rule-based algorithm for difference
unification,
and analyze its correctness, completeness, and complexity. On
the practical side, we present a novel search strategy (called
left-first search) for applying these rules in an efficient way.
Finally, we show how this algorithm can be used in new
ways to direct rippling and how it can play an important
role in theorem proving and other kinds of automated reasoning.
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-92-247.pdfMPI-I-92-247.pdfMPI-I-92-247.dvi119 KBytes; 157 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1992-247
Hide details for BibTeXBibTeX
@TECHREPORT{BasinWalsh92b,
  AUTHOR = {Basin, David A. and Walsh, Toby},
  TITLE = {Difference unification},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-92-247},
  MONTH = {November},
  YEAR = {1992},
  ISSN = {0946-011X},
}