Problem #99 (Solved !)
Originator: Konstantin Korovin and Andrei Voronkov [KV00]
Date: June 2000
Summary:
Is the firstorder theory of any KnuthBendix ordering decidable?
Is there an algorithm which, given a term signature Σ, a weight
function w and a precedence >>, decides whether a firstorder formula is
valid in the termalgebra with the KnuthBendix 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 KnuthBendix 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.
KnuthBendix constraint solving is NPcomplete.
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.
SpringerVerlag.
 [KV02a]

Konstantin Korovin and Andrei Voronkov.
The decidability of the firstorder theory of the KnuthBendix
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.
SpringerVerlag.
A preliminary report of the result appeared in [KV02b].
 [KV02b]

Konstantin Korovin and Andrei Voronkov.
The decidability of the firstorder theory of the KnuthBendix
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 0205,
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 firstorder theory of KnuthBendix 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.
SpringerVerlag.