From b542606eafae20784100a5f270109bb678dca869 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 14 Nov 2005 11:49:58 +0000 Subject: [PATCH] Introduction. --- helm/papers/matita/matita.tex | 115 +++++++++++++++++++++++++++++++--- 1 file changed, 107 insertions(+), 8 deletions(-) diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index d08175719..ab37f7849 100644 --- a/helm/papers/matita/matita.tex +++ b/helm/papers/matita/matita.tex @@ -34,7 +34,7 @@ \newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1} -\title{The proof assistant Matita} +\title{The Matita proof assistant} \author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi and Stefano Zacchiroli} \institute{Department of Computer Science, University of Bologna\\ @@ -49,6 +49,93 @@ \section{Introduction} \label{sec:intro} +{\em Matita} is the proof assistant under development by the Helm team +\cite{annals} at the University of Bologna, under the direction of +Prof.Asperti. +The origin of the system goes back to 1999. At the time we were mostly +interested to develop tools and techniques to enhance the accessibility +via web of formal libraries of mathematics. Due to its dimension, the +library of the coq proof assistant (of the order of 35000 theorems) +was choosed as a privileged test bench for our work, although experiments +have been also conducted with other systems, and notably with Nuprl. +The work, mostly performed in the framework of the recently concluded +European project IST-33562-Mowgli \cite{pechino}, mainly consisted in the +following teps: +\begin{itemize} +\item exporting the information from the internal representation of +Coq to a system and platform independent format. Since XML was at the +time an emerging standard, we naturally adopted this technology, fostering +a content-based architecture for future system, where the documents +of the library were the the main components around which everything else +has to be build; +\item developing indexing and searching techniques supporting semantic +queries to the library; these efforts gave birth to our {\em whelp} +search engine, described in \cite{whelp}; +\item developing languages and tools for a high-quality notational +rendering of mathematical information; in particular, we have been +active in the MathML Working group since 1999, and developed inside +Helm a MathML-compliant widget for the GTK graphical environment +which can be integrated in any application. +\end{itemize} +The exportation issue, extensively discussed in \cite{exportation}, +has several major implications worth to be discussed. + +The first +point concern the kind of content information to be exported. In a +proof assistant like coq, proofs are represented in at least three clearly +distinguishable formats: scripts (i.e. sequences of commands issued by the +user to the system during an interactive session of proof), proof objects +(which is the low-level representation of proofs in the form of +lambda-terms readable to and checked by kernel) and proof-trees (which +is a kind of intermediate representation, vaguely inspired by a sequent +like notation, that inherits most of the defects but essentially +none of the advantages of the previous representations). +Partially related to this problem, there is the +issue of the {\em granularity} of the library: scripts usually comprise +small developments with many definitions and theorems, while +proof objects correspond to individual mathemtical items. + +In our case, the choice of the content encoding was eventually dictated +by the methodological assumption of offering the information in a +stable and system independent format. The language of scripts is too +oriented to Coq, and it changes too rapidly to be of any interest +to third parties. On the other side, the language of proof objects +merely depend on +the logical framework (the Calculus of Inductive Constructions, in +the case of Coq), is grammatically simple, semantically clear and, +especially, is very stable (as the kernel of the proof assistants +often is). +So the granularity of the library is at the level of individual +objects, that also justifies from another point of view the need +for efficient searching techniques for retrieving individual +logical items from the repository. + +The main (possibly only) problem with proof objects is that they are +difficult to read and do not directly correspond to what the user typed +in. An analogy frequently made in the proof assistant community is that of +comparing the vernacular language of scripts to a high level source language +and lambda terms to the assembly language they are compiled in, We do not +share this view and prefer to look at scripts as an imperative language, +and to lambda terms as their denotational semantics; still, however, +denotational semantics is possibly more formal but surely not more readable +than the imperative source. + +For all the previous reasons, a huge amount of work inside Mowgli has +been devoted to automatic reconstruction of proofs in natural language +from lambda terms. Since lambda terms are in close connection +with natural deduction +(thay is still the most natural logical language discovered so far) +the work is not hopeless as it may seem, especially if rendering +is combined, as in our case, with dynamic features supporting +in-line expansions or contraction of subproofs. The final +rendering is probably not entirely satisfactory (see \cite{ida} for a +discussion), but surely +readable (the actual quality largely depends by the way the lambda +term is written). + + + + \begin{itemize} \item scelta del sistema fondazionale @@ -60,13 +147,6 @@ \end{itemize} \end{itemize} -\textbf{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. - \section{Features} \subsection{mathml} @@ -125,12 +205,31 @@ V.Tamburrelli. \subsection{localizzazione errori} \ASSIGNEDTO{} +\textbf{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{ida}A.Asperti, H.Geuvers, I.Loeb, L.E.Mamane, C.Sacerdoti Coen. + An Interactive Algebra Course with Formalised Proofs and Definitions. + Post-Proceedings of the Fourth International Conference on + Mathemtical Knowledge Management. Bremen, Germany, July 2005. LNCS, + to appear. + \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{whelp} A.~Asperti, F.~Guidi, C.~Sacerdoti Coen, + E.Tassi, S.Zacchiroli. \emph{A content based mathematical search + engine: whelp}. Post-proceedings of the Types 2004 International + Conference, Jouy-en-Josas, France, December 2004. LNCS (to appear). + \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. -- 2.39.2