Title :
A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering
Author :
Korovin, Konstantin ; Voronkov, Andrei
Author_Institution :
Dept. of Comput. Sci., Manchester Univ., UK
Abstract :
The authors show the decidability of the existential theory of term algebras with any Knuth-Bendix ordering. They achieve this by giving a procedure for solving Knuth-Bendix ordering constraints. As for complexity, NP-hardness of the set of satisfiable quantifier-free formulas can be shown in the same way as by R. Nieuwenhuis (1993). The algorithm presented does not give an NP upper bound; we point out parts of our algorithm that may cause nonpolynomial behavior
Keywords :
algebra; computability; computational complexity; decidability; decision theory; Knuth-Bendix ordering; NP upper bound; NP-hardness; complexity; decidability; decision procedure; existential theory; nonpolynomial behavior; ordering constraints; satisfiable quantifier-free formulas; term algebras; Algebra; Chromium; Computer science; Constraint theory; Equations; Reactive power; Upper bound;
Conference_Titel :
Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on
Conference_Location :
Santa Barbara, CA
Print_ISBN :
0-7695-0725-5
DOI :
10.1109/LICS.2000.855777
