\documentclass{rtaloop}
\rtalabel{kpo-theory}

\begin{document}
\begin{solvedproblem}{Konstantin Korovin and Andrei Voronkov}{\cite{korovin00lics}}{June 2000}

\begin{abstract}
  Is the first-order theory of any \emph{Knuth-Bendix ordering} decidable?
\end{abstract}

Is there an algorithm which, given a term signature $\Sigma$, 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
\begin{itemize}
\item the existential fragment \cite{korovin00lics,korovin01icalp};
\item signatures consisting only of constants and unary function symbols
  \cite{korovin02fsttcs}.
\end{itemize}

\begin{remark}
  This has been answered in the affirmative \cite{zhang05cade}.
\end{remark}
\nocite{korovin02unif}
\end{solvedproblem}

\end{document}