Problem #99 (Solved !)
Originator: Konstantin Korovin and Andrei Voronkov [KV00]
Date: June 2000
Summary:
Is the first-order theory of any Knuth-Bendix ordering decidable?
Is there an algorithm which, given a term signature Σ, a weight
function w and a precedence >>, decides whether a first-order formula is
valid in the term-algebra with the Knuth-Bendix ordering defined by (w,>>) ?
Positive partial results have been given for
-
the existential fragment [KV00, KV01];
- signatures consisting only of constants and unary function symbols
[KV02a].
Remark
This has been answered in the affirmative [ZSM05].
References
-
[KV00]
-
Konstantin Korovin and Andrei Voronkov.
A decision procedure for the existential theory of term algebras with
the Knuth-Bendix ordering.
In 15th Annual IEEE Symposium on Logic in Computer Science,
pages 291–302, Santa Barbara, CA, USA, June 2000.
IEEE.
- [KV01]
-
Konstantin Korovin and Andrei Voronkov.
Knuth-Bendix constraint solving is NP-complete.
In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors,
28th International Colloquium on Automata, Languages and Programming,
volume 2076 of Lecture Notes in Computer
Science, pages 979–992, Crete, Greece, July 2001.
Springer-Verlag.
- [KV02a]
-
Konstantin Korovin and Andrei Voronkov.
The decidability of the first-order theory of the Knuth-Bendix
orders in the case of unary signatures.
In Foundations of Software
Technology and Theoretical Computer Science,
Lecture Notes in Computer
Science, Kanpur, India, December 2002.
Springer-Verlag.
A preliminary report of the result appeared in [KV02b].
- [KV02b]
-
Konstantin Korovin and Andrei Voronkov.
The decidability of the first-order theory of the Knuth-Bendix
orders in the case of unary signatures.
In Christophe Ringeissen, Cesare Tinelli, Ralf Treinen, and Rakesh M.
Verma, editors, Proceedings of the
16th International Workshop on
Unification (UNIF 2002), Technical Report 02-05,
Department of Computer Science,
University of Iowa, pages 45–46, Copenhagen,
Denmark, July 2002.
- [ZSM05]
-
Ting Zhang, Henny Sipma, and Zohar Manna.
The
decidability of the first-order theory of Knuth-Bendix order.
In Robert Nieuwenhuis, editor, 20th International Conference on
Automated Deduction, volume 3632 of Lecture Notes in Computer
Science, pages 131–148, Tallinn, Estonia, July 2005.
Springer-Verlag.