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{\logo}[3]{
   9 %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
  10 %}
  11
  12 \newcommand{\AUTO}{\textsc{Auto}}
  13 \newcommand{\COQ}{Coq}
  14 \newcommand{\ELIM}{\textsc{Elim}}
  15 \newcommand{\HELM}{Helm}
  16 \newcommand{\HINT}{\textsc{Hint}}
  17 \newcommand{\IN}{\ensuremath{\mathbb{N}}}
  18 \newcommand{\INSTANCE}{\textsc{Instance}}
  19 \newcommand{\IR}{\ensuremath{\mathbb{R}}}
  20 \newcommand{\LIBXSLT}{LibXSLT}
  21 \newcommand{\LOCATE}{\textsc{Locate}}
  22 \newcommand{\MATCH}{\textsc{Match}}
  23 \newcommand{\MATITA}{Matita}
  24 \newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
  25 \newcommand{\MOWGLI}{MoWGLI}
  26 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
  27 \newcommand{\NATIND}{\mathit{nat\_ind}}
  28 \newcommand{\OCAML}{OCaml}
  29 \newcommand{\PROP}{\mathit{Prop}}
  30 \newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
  31 \newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
  32 \newcommand{\UWOBO}{UWOBO}
  33 \newcommand{\WHELP}{Whelp}
  34
  35 \newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
  36
  37 \title{The proof assistant Matita}
  38 \author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
  39  and Stefano Zacchiroli}
  40 \institute{Department of Computer Science, University of Bologna\\
  41  Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY\\
  42  \email{$\{$asperti,sacerdot,tassi,zacchiro$\}$@cs.unibo.it}}
  43
  44 \begin{document}
  45 \maketitle
  46
  47 \begin{abstract}
  48 \end{abstract}
  49
  50 \section{Introduction}
  51 \label{sec:intro}
  52
  53 \begin{itemize}
  54  \item scelta del sistema fondazionale
  55  \item sistema indipendente (da Coq)
  56   \begin{itemize}
  57    \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
  58     implementative, \dots)
  59    \item compatibilit\`a con sistemi legacy
  60   \end{itemize}
  61 \end{itemize}
  62
  63 \textbf{Acknowledgements}
  64 We would like to thank all the students that during the past
  65 five years collaborated in the \HELM{} project and contributed to
  66 the development of Matita, and in particular
  67 A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
  68 V.Tamburrelli.
  69
  70 \section{Features}
  71
  72 \subsection{mathml}
  73 \ASSIGNEDTO{zack}
  74
  75 \subsection{metavariabili}
  76 \ASSIGNEDTO{csc}
  77
  78 \subsection{pattern}
  79 \ASSIGNEDTO{gares}
  80
  81 \subsection{tatticali}
  82 \ASSIGNEDTO{gares}
  83
  84 \subsection{disambiguazione}
  85 \ASSIGNEDTO{zack}
  86
  87 \subsection{notazione}
  88 \ASSIGNEDTO{zack}
  89
  90 \subsection{libreria tutta visibile}
  91 \ASSIGNEDTO{csc}
  92
  93 \subsection{ricerca e indicizzazione}
  94 \ASSIGNEDTO{andrea}
  95
  96 \subsection{auto}
  97 \ASSIGNEDTO{andrea}
  98
  99 \subsection{xml / gestione della libreria}
 100 \ASSIGNEDTO{gares}
 101
 102 \subsection{named variable}
 103 \ASSIGNEDTO{csc}
 104
 105 \subsection{assenza di proof tree / resa in linguaggio naturale}
 106 \ASSIGNEDTO{andrea}
 107
 108 \subsection{selezione semantica, cut paste, hyperlink}
 109 \ASSIGNEDTO{zack}
 110
 111 \subsection{sostituzioni esplicite vs moduli}
 112 \ASSIGNEDTO{csc}
 113
 114 \section{Drawbacks, missing, \dots}
 115
 116 \subsection{moduli}
 117 \ASSIGNEDTO{}
 118
 119 \subsection{ltac}
 120 \ASSIGNEDTO{}
 121
 122 \subsection{estrazione}
 123 \ASSIGNEDTO{}
 124
 125 \subsection{localizzazione errori}
 126 \ASSIGNEDTO{}
 127
 128 \begin{thebibliography}{}
 129
 130  \bibitem{annals} A.~Asperti, F.~Guidi, L.~Padovani, C.~Sacerdoti Coen,
 131   I.~Schena. \emph{Mathematical Knowledge Management in HELM}. Annals of
 132   Mathematics and Artificial Intelligence, 38(1): 27--46; May 2003.
 133
 134  \bibitem{metadata2} A. Asperti, M. Selmi. \emph{Efficient Retrieval of
 135   Mathematical Statements}. In Proceeding of the Third International Conference
 136   on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland. LNCS 3119.
 137  \bibitem{pechino} A.Asperti, B.Wegner. \emph{An Approach to
 138   Machine-Understandable Representation of the Mathematical Information in
 139   Digital Documents}.  In: Fengshai Bai and Bernd Wegner (eds.): Electronic
 140   Information and Communication in Mathematics, LNCS vol. 2730,
 141   pp. 14--23, 2003
 142
 143  \bibitem{coq} The Coq proof-assistant, \url{http://coq.inria.fr}
 144
 145  \bibitem{metadata1} F. Guidi, C. Sacerdoti Coen. \emph{Querying Distributed
 146   Digital Libraries of Mathematics}. In Proceedings of Calculemus 2003, 11th
 147   Symposium on the Integration of Symbolic Computation and Mechanized
 148   Reasoning. Aracne Editrice.
 149
 150  \bibitem{exportation} C. Sacerdoti Coen. \emph{From Proof-Assistans to
 151   Distributed Libraries of Mathematics: Tips and Pitfalls}.
 152   In Proc. Mathematical Knowledge Management 2003, Lecture Notes in Computer
 153   Science, Vol. 2594, pp. 30--44, Springer-Verlag.
 154
 155  \bibitem{disambiguation} C. Sacerdoti Coen, S. Zacchiroli. \emph{Efficient
 156   Ambiguous Parsing of Mathematical Formulae}. In Proceedings of the Third
 157   International Conference on Mathematical Knowledge Management, MKM 2004.
 158   LNCS,3119.
 159
 160 \end{thebibliography}
 161
 162 \end{document}
 163