From 6be8977d7ade4cb6715810ada090e16deeb8c2f0 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 10 Nov 2005 10:02:20 +0000
Subject: [PATCH] Headings of the matita paper.

---
 helm/papers/matita/matita.tex | 92 +++++++++++++++++++++++++++++++++++
 1 file changed, 92 insertions(+)
 create mode 100644 helm/papers/matita/matita.tex

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
new file mode 100644
index 000000000..78b35679c
--- /dev/null
+++ b/helm/papers/matita/matita.tex
@@ -0,0 +1,92 @@
+\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, Ferruccio Guidi, Claudio Sacerdoti Coen
+ 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}
+
-- 
2.39.2