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


Difference matching

Basin, David A. and Walsh, Toby

MPI-I-92-211. March 1992, 12 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
Difference matching is a generalization of first-order matching where terms are made identical both by variable instantiation and by structure hiding. After matching, the hidden structure may be removed by a type of controlled rewriting, called rippling, that leaves the rest of the term unaltered. Rippling has proved highly successful in inductive theorem proving. Difference matching allows us to use rippling in other contexts, e.g., equational,
inequational, and propositional reasoning. We present a difference matching algorithm, its properties, several
applications, and suggest extensions.
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-211.pdfMPI-I-92-211.pdfMPI-I-92-211.dvi63 KBytes; 122 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:
Hide details for BibTeXBibTeX
  AUTHOR = {Basin, David A. and Walsh, Toby},
  TITLE = {Difference matching},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-92-211},
  MONTH = {March},
  YEAR = {1992},
  ISSN = {0946-011X},