\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\\
\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
\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}
\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.
projects / helm.git / commitdiff