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

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

On Using Ground Joinable Equations in Equational Theorem Proving

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

Hillenbrand,  Thomas
International Max Planck Research School, MPI for Informatics, Max Planck Society;
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

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

Löchner,  Bernd
Programming Logics, MPI for Informatics, Max Planck Society;

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

Avenhaus, J., Hillenbrand, T., & Löchner, B. (2003). On Using Ground Joinable Equations in Equational Theorem Proving. Journal of Symbolic Computation, 36, 217-233.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-2DA8-E
Zusammenfassung
When rewriting and completion techniques are used for equational theorem proving, the axiom set is saturated with the aim to get a rewrite system that is terminating and confluent on ground terms. To reduce the computational effort it should (1) be powerful for rewriting and (2) create not too many critical pairs. These problems become especially important if some operators are associative and commutative (\AC). We show in this paper how these two goals can be reached to some extent by using ground joinable equations for simplification purposes and omitting them from the generation of new facts. % For the special case of \AC-operators we present a simple redundancy criterion which is easy to implement, efficient, and effective in practice, leading to significant speed-ups.