1 \documentclass[a4paper]{llncs}
4 \usepackage{amssymb,amsmath}
8 %\newcommand{\logo}[3]{
9 %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
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}
35 \newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
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}}
50 \section{Introduction}
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
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
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
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.
80 The exportation issue, extensively discussed in \cite{exportation},
81 has several major implications worth to be discussed.
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.
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
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
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.
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.
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
141 \item scelta del sistema fondazionale
142 \item sistema indipendente (da Coq)
144 \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
145 implementative, \dots)
146 \item compatibilit\`a con sistemi legacy
155 \subsection{metavariabili}
161 \subsection{tatticali}
164 \subsection{disambiguazione}
167 \subsection{notazione}
170 \subsection{libreria tutta visibile}
173 \subsection{ricerca e indicizzazione}
179 \subsection{xml / gestione della libreria}
182 \subsection{named variable}
185 \subsection{assenza di proof tree / resa in linguaggio naturale}
188 \subsection{selezione semantica, cut paste, hyperlink}
191 \subsection{sostituzioni esplicite vs moduli}
194 \section{Drawbacks, missing, \dots}
202 \subsection{estrazione}
205 \subsection{localizzazione errori}
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,
216 \begin{thebibliography}{}
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,
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.
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).
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,
242 \bibitem{coq} The Coq proof-assistant, \url{http://coq.inria.fr}
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.
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.
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.
259 \end{thebibliography}