\documentclass{rtaloop}

\begin{document}
\begin{problem}{John Pedersen}{}{April 1991} 

\begin{abstract}
Is there a finite term-rewriting system of some kind for free lattices?
\end{abstract}

Is there a finite term-rewriting system of some kind for free lattices?

\begin{remark}
As mentioned in a remark to \rtaref{trs-lattices}, it has been shown in
\cite{freese93pc} that there is no finite, normal form,
associative-commutative term-rewriting system for lattices.
\end{remark}

\begin{submitted}{Jordi Levy}{Fri Apr 17 20:20:41 MET DST 1998}

There are bi-rewriting systems for free lattices and distributive free
lattices \cite{LevyAgust:jsc96}. Bi-rewriting systems are used to automatize
deduction in theories with monotonic order relations. They are composed of a
pair of rewriting systems. One is used for rewriting terms into smaller terms,
and the other for rewriting terms into bigger terms.

\end{submitted}

\end{problem}
\end{document}