\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage[english]{babel}
\usepackage{eufrak}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions}
\author{Dmitriy Traytel and Tobias Nipkow}
\maketitle

\begin{abstract}
  Monadic second-order logic on finite words (MSO) is a decidable yet expressive
  logic into which many decision problems can be encoded. Since MSO formulas
  correspond to regular languages, equivalence of MSO formulas can be reduced to
  the equivalence of some regular structures (e.g.\ automata). We verify an
  executable decision procedure for MSO formulas that is not based on automata
  but on regular expressions.

  Decision procedures for regular expression equivalence have been formalized
  before (e.g.\ in Isabelle/HOL~\cite{KraussN-AFP}), usually based on Brzozowski
  derivatives. Yet, for a straightforward embedding of MSO formulas into regular
  expressions an extension of regular expressions with a projection operation is
  required. We prove total correctness and completeness of an equivalence
  checker for regular expressions extended in that way. We also define a
  language-preserving translation of formulas into regular expressions with
  respect to two different semantics of MSO.

  The formalization is described in the ICFP 2013 functional
  pearl~\cite{TraytelN-ICFP13}.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
