MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


Difference unification

Basin, David A. and Walsh, Toby

November 1992, 15 pages.

Status: available - back from printing

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.

  • MPI-I-92-247.pdfMPI-I-92-247.pdfMPI-I-92-247.dvi
  • Attachement: MPI-I-92-247.dvi (119 KBytes); MPI-I-92-247.pdf (157 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  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},