\documentclass[a4paper]{llncs}
\pagestyle{headings}
\usepackage{graphicx}
\usepackage{amssymb,amsmath}
\usepackage{hyperref}
\usepackage{picins}

%\newcommand{\logo}[3]{
%\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
%}

\newcommand{\AUTO}{\textsc{Auto}}
\newcommand{\COQ}{Coq}
\newcommand{\ELIM}{\textsc{Elim}}
\newcommand{\HELM}{Helm}
\newcommand{\HINT}{\textsc{Hint}}
\newcommand{\IN}{\ensuremath{\mathbb{N}}}
\newcommand{\INSTANCE}{\textsc{Instance}}
\newcommand{\IR}{\ensuremath{\mathbb{R}}}
\newcommand{\LIBXSLT}{LibXSLT}
\newcommand{\LOCATE}{\textsc{Locate}}
\newcommand{\MATCH}{\textsc{Match}}
\newcommand{\MATITA}{Matita}
\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
\newcommand{\MOWGLI}{MoWGLI}
\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
\newcommand{\NATIND}{\mathit{nat\_ind}}
\newcommand{\OCAML}{OCaml}
\newcommand{\PROP}{\mathit{Prop}}
\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
\newcommand{\UWOBO}{UWOBO}
\newcommand{\WHELP}{Whelp}

\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}

\title{The proof assistant Matita}
\author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
 and Stefano Zacchiroli}
\institute{Department of Computer Science, University of Bologna\\
 Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY\\
 \email{$\{$asperti,sacerdot,tassi,zacchiro$\}$@cs.unibo.it}}

\begin{document}
\maketitle

\begin{abstract}
\end{abstract}

\section{Introduction}
\label{sec:intro}

\begin{itemize}
 \item scelta del sistema fondazionale
 \item sistema indipendente (da Coq)
  \begin{itemize}
   \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
    implementative, \dots)
   \item compatibilit\`a con sistemi legacy
  \end{itemize}
\end{itemize}

\textbf{Acknowledgements}
We would like to thank all the students that during the past
five years collaborated in the \HELM{} project and contributed to 
the development of Matita, and in particular
A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi, 
V.Tamburrelli.

\section{Features}

\subsection{mathml}
\ASSIGNEDTO{zack}

\subsection{metavariabili}
\ASSIGNEDTO{csc}

\subsection{pattern}
\ASSIGNEDTO{gares}

\subsection{tatticali}
\ASSIGNEDTO{gares}

\subsection{disambiguazione}
\ASSIGNEDTO{zack}

\subsection{notazione}
\ASSIGNEDTO{zack}

\subsection{libreria tutta visibile}
\ASSIGNEDTO{csc}

\subsection{ricerca e indicizzazione}
\ASSIGNEDTO{andrea}

\subsection{auto}
\ASSIGNEDTO{andrea}

\subsection{xml / gestione della libreria}
\ASSIGNEDTO{gares}

\subsection{named variable}
\ASSIGNEDTO{csc}

\subsection{assenza di proof tree / resa in linguaggio naturale}
\ASSIGNEDTO{andrea}

\subsection{selezione semantica, cut paste, hyperlink}
\ASSIGNEDTO{zack}

\subsection{sostituzioni esplicite vs moduli}
\ASSIGNEDTO{csc}

\section{Drawbacks, missing, \dots}

\subsection{moduli}
\ASSIGNEDTO{}

\subsection{ltac}
\ASSIGNEDTO{}

\subsection{estrazione}
\ASSIGNEDTO{}

\subsection{localizzazione errori}
\ASSIGNEDTO{}

\begin{thebibliography}{}

 \bibitem{annals} A.~Asperti, F.~Guidi, L.~Padovani, C.~Sacerdoti Coen,
  I.~Schena. \emph{Mathematical Knowledge Management in HELM}. Annals of
  Mathematics and Artificial Intelligence, 38(1): 27--46; May 2003.

 \bibitem{metadata2} A. Asperti, M. Selmi. \emph{Efficient Retrieval of
  Mathematical Statements}. In Proceeding of the Third International Conference
  on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland. LNCS 3119.
 \bibitem{pechino} A.Asperti, B.Wegner. \emph{An Approach to
  Machine-Understandable Representation of the Mathematical Information in
  Digital Documents}.  In: Fengshai Bai and Bernd Wegner (eds.): Electronic
  Information and Communication in Mathematics, LNCS vol. 2730, 
  pp. 14--23, 2003

 \bibitem{coq} The Coq proof-assistant, \url{http://coq.inria.fr}

 \bibitem{metadata1} F. Guidi, C. Sacerdoti Coen. \emph{Querying Distributed
  Digital Libraries of Mathematics}. In Proceedings of Calculemus 2003, 11th
  Symposium on the Integration of Symbolic Computation and Mechanized 
  Reasoning. Aracne Editrice.
 
 \bibitem{exportation} C. Sacerdoti Coen. \emph{From Proof-Assistans to
  Distributed Libraries of Mathematics: Tips and Pitfalls}.
  In Proc. Mathematical Knowledge Management 2003, Lecture Notes in Computer
  Science, Vol. 2594, pp. 30--44, Springer-Verlag.

 \bibitem{disambiguation} C. Sacerdoti Coen, S. Zacchiroli. \emph{Efficient
  Ambiguous Parsing of Mathematical Formulae}. In Proceedings of the Third
  International Conference on Mathematical Knowledge Management, MKM 2004. 
  LNCS,3119.

\end{thebibliography}

\end{document}

