\documentclass{rtaloop}
\rtalabel{ordered-paramodulation}

\begin{document}
\begin{solvedproblem}{Micha\"el Rusinowitch}{}{April 1995}

\begin{abstract}
Can the restrictions on orderings for the use in ordered theorem proving
strategies be relaxed?
\end{abstract}

Ordered paramodulation is known to be complete for simplification orderings
that are total on ground terms \cite{HR86:cade}.
Other theorem proving strategies are similarly restricted.
How can these restrictions be relaxed?


\begin{remark}
\cite{bofill:lics99} shows that it is sufficient for the ordering to be
well-founded and to have the subterm property.
\end{remark}

\end{solvedproblem}
\end{document}