From 6be8977d7ade4cb6715810ada090e16deeb8c2f0 Mon Sep 17 00:00:00 2001 From: Andrea Asperti 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