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 Matita proof assistant}
  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 {\em Matita} is the proof assistant under development by the Helm team
  53 \cite{annals} at the University of Bologna, under the direction of
  54 Prof.Asperti.
  55 The origin of the system goes back to 1999. At the time we were mostly
  56 interested to develop tools and techniques to enhance the accessibility
  57 via web of formal libraries of mathematics. Due to its dimension, the
  58 library of the coq proof assistant (of the order of 35000 theorems)
  59 was choosed as a privileged test bench for our work, although experiments
  60 have been also conducted with other systems, and notably with Nuprl.
  61 The work, mostly performed in the framework of the recently concluded
  62 European project IST-33562-Mowgli \cite{pechino}, mainly consisted in the
  63 following teps:
  64 \begin{itemize}
  65 \item exporting the information from the internal representation of
  66 Coq to a system and platform independent format. Since XML was at the
  67 time an emerging standard, we naturally adopted this technology, fostering
  68 a content-based architecture for future system, where the documents
  69 of the library were the the main components around which everything else
  70 has to be build;
  71 \item developing indexing and searching techniques supporting semantic
  72 queries to the library; these efforts gave birth to our {\em whelp}
  73 search engine, described in \cite{whelp};
  74 \item developing languages and tools for a high-quality notational
  75 rendering of mathematical information; in particular, we have been
  76 active in the MathML Working group since 1999, and developed inside
  77 Helm a MathML-compliant widget for the GTK graphical environment
  78 which can be integrated in any application.
  79 \end{itemize}
  80 The exportation issue, extensively discussed in \cite{exportation},
  81 has several major implications worth to be discussed.
  82
  83 The first
  84 point concern the kind of content information to be exported. In a
  85 proof assistant like coq, proofs are represented in at least three clearly
  86 distinguishable formats: scripts (i.e. sequences of commands issued by the
  87 user to the system during an interactive session of proof), proof objects
  88 (which is the low-level representation of proofs in the form of
  89 lambda-terms readable to and checked by kernel) and proof-trees (which
  90 is a kind of intermediate representation, vaguely inspired by a sequent
  91 like notation, that inherits most of the defects but essentially
  92 none of the advantages of the previous representations).
  93 Partially related to this problem, there is the
  94 issue of the {\em granularity} of the library: scripts usually comprise
  95 small developments with many definitions and theorems, while
  96 proof objects correspond to individual mathemtical items.
  97
  98 In our case, the choice of the content encoding was eventually dictated
  99 by the methodological assumption of offering the information in a
 100 stable and system independent format. The language of scripts is too
 101 oriented to Coq, and it changes too rapidly to be of any interest
 102 to third parties. On the other side, the language of proof objects
 103 merely depend on
 104 the logical framework (the Calculus of Inductive Constructions, in
 105 the case of Coq), is grammatically simple, semantically clear and,
 106 especially, is very stable (as the kernel of the proof assistants
 107 often is).
 108 So the granularity of the library is at the level of individual
 109 objects, that also justifies from another point of view the need
 110 for efficient searching techniques for retrieving individual
 111 logical items from the repository.
 112
 113 The main (possibly only) problem with proof objects is that they are
 114 difficult to read and do not directly correspond to what the user typed
 115 in. An analogy frequently made in the proof assistant community is that of
 116 comparing the vernacular language of scripts to a high level source language
 117 and lambda terms to the assembly language they are compiled in, We do not
 118 share this view and prefer to look at scripts as an imperative language,
 119 and to lambda terms as their denotational semantics; still, however,
 120 denotational semantics is possibly more formal but surely not more readable
 121 than the imperative source.
 122
 123 For all the previous reasons, a huge amount of work inside Mowgli has
 124 been devoted to automatic reconstruction of proofs in natural language
 125 from lambda terms. Since lambda terms are in close connection
 126 with natural deduction
 127 (thay is still the most natural logical language discovered so far)
 128 the work is not hopeless as it may seem, especially if rendering
 129 is combined, as in our case, with dynamic features supporting
 130 in-line expansions or contraction of subproofs. The final
 131 rendering is probably not entirely satisfactory (see \cite{ida} for a
 132 discussion), but surely
 133 readable (the actual quality largely depends by the way the lambda
 134 term is written).
 135
 136
 137
 138
 139
 140 \begin{itemize}
 141  \item scelta del sistema fondazionale
 142  \item sistema indipendente (da Coq)
 143   \begin{itemize}
 144    \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
 145     implementative, \dots)
 146    \item compatibilit\`a con sistemi legacy
 147   \end{itemize}
 148 \end{itemize}
 149
 150 \section{Features}
 151
 152 \subsection{mathml}
 153 \ASSIGNEDTO{zack}
 154
 155 \subsection{metavariabili}
 156 \ASSIGNEDTO{csc}
 157
 158 \subsection{pattern}
 159 \ASSIGNEDTO{gares}
 160
 161 \subsection{tatticali}
 162 \ASSIGNEDTO{gares}
 163
 164 \subsection{disambiguazione}
 165 \ASSIGNEDTO{zack}
 166
 167 \subsection{notazione}
 168 \ASSIGNEDTO{zack}
 169
 170 \subsection{libreria tutta visibile}
 171 \ASSIGNEDTO{csc}
 172
 173 \subsection{ricerca e indicizzazione}
 174 \ASSIGNEDTO{andrea}
 175
 176 \subsection{auto}
 177 \ASSIGNEDTO{andrea}
 178
 179 \subsection{xml / gestione della libreria}
 180 \ASSIGNEDTO{gares}
 181
 182 \subsection{named variable}
 183 \ASSIGNEDTO{csc}
 184
 185 \subsection{assenza di proof tree / resa in linguaggio naturale}
 186 \ASSIGNEDTO{andrea}
 187
 188 \subsection{selezione semantica, cut paste, hyperlink}
 189 \ASSIGNEDTO{zack}
 190
 191 \subsection{sostituzioni esplicite vs moduli}
 192 \ASSIGNEDTO{csc}
 193
 194 \section{Drawbacks, missing, \dots}
 195
 196 \subsection{moduli}
 197 \ASSIGNEDTO{}
 198
 199 \subsection{ltac}
 200 \ASSIGNEDTO{}
 201
 202 \subsection{estrazione}
 203 \ASSIGNEDTO{}
 204
 205 \subsection{localizzazione errori}
 206 \ASSIGNEDTO{}
 207
 208 \textbf{Acknowledgements}
 209 We would like to thank all the students that during the past
 210 five years collaborated in the \HELM{} project and contributed to
 211 the development of Matita, and in particular
 212 A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
 213 V.Tamburrelli.
 214
 215
 216 \begin{thebibliography}{}
 217
 218  \bibitem{ida}A.Asperti, H.Geuvers, I.Loeb, L.E.Mamane, C.Sacerdoti Coen.
 219   An Interactive Algebra Course with Formalised Proofs and Definitions.
 220   Post-Proceedings of the Fourth International Conference on
 221   Mathemtical Knowledge Management. Bremen, Germany, July 2005. LNCS,
 222   to appear.
 223
 224  \bibitem{annals} A.~Asperti, F.~Guidi, L.~Padovani, C.~Sacerdoti Coen,
 225   I.~Schena. \emph{Mathematical Knowledge Management in HELM}. Annals of
 226   Mathematics and Artificial Intelligence, 38(1): 27--46; May 2003.
 227
 228  \bibitem{whelp} A.~Asperti, F.~Guidi, C.~Sacerdoti Coen,
 229   E.Tassi, S.Zacchiroli. \emph{A content based mathematical search
 230   engine: whelp}. Post-proceedings of the Types 2004 International
 231   Conference, Jouy-en-Josas, France, December 2004. LNCS (to appear).
 232
 233  \bibitem{metadata2} A. Asperti, M. Selmi. \emph{Efficient Retrieval of
 234   Mathematical Statements}. In Proceeding of the Third International Conference
 235   on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland. LNCS 3119.
 236  \bibitem{pechino} A.Asperti, B.Wegner. \emph{An Approach to
 237   Machine-Understandable Representation of the Mathematical Information in
 238   Digital Documents}.  In: Fengshai Bai and Bernd Wegner (eds.): Electronic
 239   Information and Communication in Mathematics, LNCS vol. 2730,
 240   pp. 14--23, 2003
 241
 242  \bibitem{coq} The Coq proof-assistant, \url{http://coq.inria.fr}
 243
 244  \bibitem{metadata1} F. Guidi, C. Sacerdoti Coen. \emph{Querying Distributed
 245   Digital Libraries of Mathematics}. In Proceedings of Calculemus 2003, 11th
 246   Symposium on the Integration of Symbolic Computation and Mechanized
 247   Reasoning. Aracne Editrice.
 248
 249  \bibitem{exportation} C. Sacerdoti Coen. \emph{From Proof-Assistans to
 250   Distributed Libraries of Mathematics: Tips and Pitfalls}.
 251   In Proc. Mathematical Knowledge Management 2003, Lecture Notes in Computer
 252   Science, Vol. 2594, pp. 30--44, Springer-Verlag.
 253
 254  \bibitem{disambiguation} C. Sacerdoti Coen, S. Zacchiroli. \emph{Efficient
 255   Ambiguous Parsing of Mathematical Formulae}. In Proceedings of the Third
 256   International Conference on Mathematical Knowledge Management, MKM 2004.
 257   LNCS,3119.
 258
 259 \end{thebibliography}
 260
 261 \end{document}
 262