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

\newcommand{\whelp}{Whelp}

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

\newcommand{\coq}{Coq}
\newcommand{\mowgli}{MoWGLI}
\newcommand{\IR}{\ensuremath{\mathbb{R}}}
\newcommand{\IN}{\ensuremath{\mathbb{N}}}
\newcommand{\instance}{\textsc{Instance}}
\newcommand{\auto}{\textsc{Auto}}
\newcommand{\hint}{\textsc{Hint}}
\newcommand{\locate}{\textsc{Locate}}
\newcommand{\elim}{\textsc{Elim}}
\newcommand{\match}{\textsc{Match}}
\newcommand{\texmacro}[1]{\texttt{\char92 #1}}
\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
\newcommand{\Prop}{\mathit{Prop}}
\newcommand{\natind}{\mathit{nat\_ind}}
\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
\newcommand{\LIBXSLT}{LibXSLT}
\newcommand{\OCAML}{OCaml}
\newcommand{\UWOBO}{UWOBO}

\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}

{\bf 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.

\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}

