loading...
Orienting Equalities with the Knuth-Bendix Order
Ottawa, Canada June 22-June 25
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2003.121004718th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Konstantin Korovin, MPI Informatik
Andrei Voronkov, University of Manchester
Orientability of systems of equalities is the following problem: given a system of equalities s1 \simeq t1,...,n \simeq tn, does there exist a simplification ordering \succ which orients the system, that is for every i \in {1,..., n}, either si \succ ti or ti \succ si. 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.
Citation:
Konstantin Korovin, Andrei Voronkov, "Orienting Equalities with the Knuth-Bendix Order," lics, pp.75, 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.


Suggestions