helm/papers/matita/matita.tex

   1 \documentclass[a4paper]{llncs}
   2 \pagestyle{headings}
   3 \usepackage{graphicx}
   4 \usepackage{amssymb,amsmath}
   5 \usepackage{hyperref}
   6 \usepackage{picins}
   7
   8 \newcommand{\whelp}{Whelp}
   9
  10 %\newcommand{\logo}[3]{
  11 %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
  12 %}
  13
  14 \newcommand{\coq}{Coq}
  15 \newcommand{\mowgli}{MoWGLI}
  16 \newcommand{\IR}{\ensuremath{\mathbb{R}}}
  17 \newcommand{\IN}{\ensuremath{\mathbb{N}}}
  18 \newcommand{\instance}{\textsc{Instance}}
  19 \newcommand{\auto}{\textsc{Auto}}
  20 \newcommand{\hint}{\textsc{Hint}}
  21 \newcommand{\locate}{\textsc{Locate}}
  22 \newcommand{\elim}{\textsc{Elim}}
  23 \newcommand{\match}{\textsc{Match}}
  24 \newcommand{\texmacro}[1]{\texttt{\char92 #1}}
  25 \newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
  26 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
  27 \newcommand{\Prop}{\mathit{Prop}}
  28 \newcommand{\natind}{\mathit{nat\_ind}}
  29 \newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
  30 \newcommand{\LIBXSLT}{LibXSLT}
  31 \newcommand{\OCAML}{OCaml}
  32 \newcommand{\UWOBO}{UWOBO}
  33
  34 \title{The proof assistant Matita}
  35 \author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
  36  and Stefano Zacchiroli}
  37 \institute{Department of Computer Science, University of Bologna\\
  38  Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY\\
  39  \email{$\{$asperti,sacerdot,tassi,zacchiro$\}$@cs.unibo.it}}
  40
  41 \begin{document}
  42 \maketitle
  43
  44 \begin{abstract}
  45 \end{abstract}
  46
  47 \section{Introduction}
  48 \label{sec:intro}
  49
  50 {\bf Acknowledgements}
  51 We would like to thank all the students that during the past
  52 five years collaborated in the Helm project and contributed to
  53 the development of Matita, and in particular
  54 A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
  55 V.Tamburrelli.
  56
  57 \begin{thebibliography}{}
  58
  59  \bibitem{annals} A.~Asperti, F.~Guidi, L.~Padovani, C.~Sacerdoti Coen,
  60   I.~Schena. \emph{Mathematical Knowledge Management in HELM}. Annals of
  61   Mathematics and Artificial Intelligence, 38(1): 27--46; May 2003.
  62
  63  \bibitem{metadata2} A. Asperti, M. Selmi. \emph{Efficient Retrieval of
  64   Mathematical Statements}. In Proceeding of the Third International Conference
  65   on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland. LNCS 3119.
  66  \bibitem{pechino} A.Asperti, B.Wegner. \emph{An Approach to
  67   Machine-Understandable Representation of the Mathematical Information in
  68   Digital Documents}.  In: Fengshai Bai and Bernd Wegner (eds.): Electronic
  69   Information and Communication in Mathematics, LNCS vol. 2730,
  70   pp. 14--23, 2003
  71
  72  \bibitem{coq} The Coq proof-assistant, \url{http://coq.inria.fr}
  73
  74  \bibitem{metadata1} F. Guidi, C. Sacerdoti Coen. \emph{Querying Distributed
  75   Digital Libraries of Mathematics}. In Proceedings of Calculemus 2003, 11th
  76   Symposium on the Integration of Symbolic Computation and Mechanized
  77   Reasoning. Aracne Editrice.
  78
  79  \bibitem{exportation} C. Sacerdoti Coen. \emph{From Proof-Assistans to
  80   Distributed Libraries of Mathematics: Tips and Pitfalls}.
  81   In Proc. Mathematical Knowledge Management 2003, Lecture Notes in Computer
  82   Science, Vol. 2594, pp. 30--44, Springer-Verlag.
  83
  84  \bibitem{disambiguation} C. Sacerdoti Coen, S. Zacchiroli. \emph{Efficient
  85   Ambiguous Parsing of Mathematical Formulae}. In Proceedings of the Third
  86   International Conference on Mathematical Knowledge Management, MKM 2004.
  87   LNCS,3119.
  88
  89 \end{thebibliography}
  90
  91 \end{document}
  92