MPI-I-92-211
Difference matching
Basin, David A. and Walsh, Toby
March 1992, 12 pages.
.
Status: available - back from printing
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.
-
MPI-I-92-211.pdf
- Attachement: MPI-I-92-211.dvi (63 KBytes); MPI-I-92-211.pdf (122 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1992-211
BibTeX
@TECHREPORT{BasinWalsh92a,
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},
}