The Community for Technology Leaders
Logic in Computer Science, Symposium on (2003)
Ottawa, Canada
June 22, 2003 to June 25, 2003
ISSN: 1043-6871
ISBN: 0-7695-1884-2
pp: 75
Konstantin Korovin , MPI Informatik
Andrei Voronkov , University of Manchester
ABSTRACT
Orientability of systems of equalities is the following problem: given a system of equalities s<sub>1</sub> \simeq t<sub>1</sub>,...,<sub>n</sub> \simeq t<sub>n</sub>, does there exist a simplification ordering \succ which orients the system, that is for every i \in {1,..., n}, either s<sub>i</sub> \succ t<sub>i</sub> or t<sub>i</sub> \succ s<sub>i</sub>. 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.
INDEX TERMS
null
CITATION
Konstantin Korovin, Andrei Voronkov, "Orienting Equalities with the Knuth-Bendix Order", Logic in Computer Science, Symposium on, vol. 00, no. , pp. 75, 2003, doi:10.1109/LICS.2003.1210047
79 ms
(Ver 3.3 (11022016))