\documentclass{rtaloop}
\rtalabel{ground-reducibility}

\begin{document}
\begin{solvedproblem}{Deepak Kapur}{}{April 1991}

\begin{abstract}
What is the complexity of deciding ground-reducibility?
\end{abstract}

A term $t$ is {\em ground reducible} with respect to a rewrite system $R$
if all its ground (variable-free) instances contain a redex.
Ground reducibility is decidable for ordinary rewriting (and finite $R$)
\cite{C88:grenoble,KNZ87:acta,P85:ic},
but $n^{n^n}$ is the best known upper bound in general,
$2^{d n \log n}$ and
$2^{c n/ \log n}$
are the best upper and lower bounds, respectively, for left-linear systems,
where $n$ is the size of the system $R$ and $c,d$ are
constants \cite{KNZ87:acta}.
Can these bounds be improved?

\begin{remark}
Ground-reducibility is EXPTIME-complete \cite{comon97lics,ComonJacquemard2003}.
\end{remark}

\end{solvedproblem}
\end{document}