Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #556 | |
|---|---|
| Title: | Difference Matching |
| Authors: | Basin,D; Walsh,T |
| Date: | 1991 |
| Presented: | Submitted to CADE-11, June, 1992 |
| Keywords: | |
| Abstract: | Difference matching is a generalization of first-order matching where terms are made identical not only by variable instantiation but also 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. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}