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

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

AC-compatible Knuth-Bendix Order

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

Korovin,  Konstantin
Programming Logics, MPI for Informatics, Max Planck Society;

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

Voronkov,  Andrei
Programming Logics, MPI for Informatics, Max Planck Society;

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

Baader,  Franz
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

Korovin, K., & Voronkov, A. (2003). AC-compatible Knuth-Bendix Order. In Automated deduction, CADE-19: 19th International Conference on Automated Deduction (pp. 47-59). Berlin, Germany: Springer.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-2BD8-3
Zusammenfassung
We introduce a family of AC-compatible Knuth-Bendix simplification orderings which are AC-total on ground terms. Our orderings preserve attractive features of the original Knuth-Bendix orderings such as polynomial algorithm for comparing terms; the orderings admit computationally efficient approximations like checking weights of terms; and prefer light terms to heavy ones. This makes them especially suited for automated deduction where efficient treatment of orderings is desirable.