de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Difference matching

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44075

Basin,  David
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45692

Walsh,  Toby
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

MPI-I-92-211.pdf
(beliebiger Volltext), 123KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Basin, D., & Walsh, T.(1992). Difference matching (MPI-I-92-211). Saarbrücken: Max-Planck-Institut für Informatik.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-B1C3-8
Zusammenfassung
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.