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

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

Orienting Equalities with the 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;

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). Orienting Equalities with the Knuth-Bendix Order. In 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03) (pp. 75-84). Los Alamitos, USA: IEEE.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-2DB0-9
Zusammenfassung
Orientability of systems of equalities is the following problem: given a system of equalities $s_1 \eql t_1, \ldots, s_n \eql t_n$, does there exist a simplification ordering $\succ$ which orients the system, that is for every $i \in \{1,...,n\}$, either $s_i \succ t_i$ or $t_i \succ s_i$. This problem can be used in rewriting for finding a canonical rewrite system for a system of equalities and in theorem proving for adjusting simplification orderings during completion. We prove that (rather surprisingly) the problem can be solved in polynomial time when we restrict ourselves to the Knuth-Bendix orderings.