\documentclass{rtaloop}


\begin{document}
\begin{problem}{Bruno Courcelle}{}{January 2005}

\begin{abstract}
  Investigate normalization by a canonical term rewrite system in the setting
  of second-order monadic logic
\end{abstract}

Consider a confluent and terminating term rewriting system and the mapping
from a term to its normal form. When is this mapping a monadic second-order
transduction? When does it preserve decidability of the monadic second-order
theory of a set of terms?

See \cite{Courcelle:tcs94,CourcelleKnapik02tcs}
\end{problem}
\end{document}