\usepackage{hyperref}
\usepackage{picins}
-\newcommand{\whelp}{Whelp}
-
%\newcommand{\logo}[3]{
%\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
%}
-\newcommand{\coq}{Coq}
-\newcommand{\mowgli}{MoWGLI}
-\newcommand{\IR}{\ensuremath{\mathbb{R}}}
+\newcommand{\AUTO}{\textsc{Auto}}
+\newcommand{\COQ}{Coq}
+\newcommand{\ELIM}{\textsc{Elim}}
+\newcommand{\HELM}{Helm}
+\newcommand{\HINT}{\textsc{Hint}}
\newcommand{\IN}{\ensuremath{\mathbb{N}}}
-\newcommand{\instance}{\textsc{Instance}}
-\newcommand{\auto}{\textsc{Auto}}
-\newcommand{\hint}{\textsc{Hint}}
-\newcommand{\locate}{\textsc{Locate}}
-\newcommand{\elim}{\textsc{Elim}}
-\newcommand{\match}{\textsc{Match}}
-\newcommand{\texmacro}[1]{\texttt{\char92 #1}}
-\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
-\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
-\newcommand{\Prop}{\mathit{Prop}}
-\newcommand{\natind}{\mathit{nat\_ind}}
-\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
+\newcommand{\INSTANCE}{\textsc{Instance}}
+\newcommand{\IR}{\ensuremath{\mathbb{R}}}
\newcommand{\LIBXSLT}{LibXSLT}
+\newcommand{\LOCATE}{\textsc{Locate}}
+\newcommand{\MATCH}{\textsc{Match}}
+\newcommand{\MATITA}{Matita}
+\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
+\newcommand{\MOWGLI}{MoWGLI}
+\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
+\newcommand{\NATIND}{\mathit{nat\_ind}}
\newcommand{\OCAML}{OCaml}
+\newcommand{\PROP}{\mathit{Prop}}
+\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
+\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
\newcommand{\UWOBO}{UWOBO}
+\newcommand{\WHELP}{Whelp}
-\title{The proof assistant Matita}
+\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
+
+\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).
+
+Summing up, we already disposed of the following tools/techniques:
+\begin{itemize}
+\item XML specifications for the Calculus of Inductive Constructions,
+with tools for parsing and saving mathematical objects in such a format;
+\item metadata specifications and tools for indexing and querying the
+XML knowledge base;
+\item a proof checker (i.e. the {\em kernel} of a proof assistant),
+implemented to check that we exported form the coq library all the
+logically relevant content;
+\item a sophisticated parser (used by the search engine), able to deal
+with potentially ambiguous and incomplete information, typical of the
+mathematical notation \cite{};
+\item a {\em refiner}, i.e. a type inference system, based on complex
+existential variables, used by the disambiguating parser;
+\item complex transformation algorithms for proof rendering in natural
+language;
+\item an innovative rendering widget, supporting high-quality bidimensional
+rendering, and semantic selection, i.e. the possibility to select semantically
+meaningfull rendering expressions, and to past the respective contebt into
+a different text area.
+\end{itemize}
+Starting from all this, the further step of developing our own
+proof assistant was too
+small and too tempting to be neglected. Essentially, we ``just'' had to
+add an authoring interface, and a set of functionalities for the
+overall management of the library, integrating everything into a
+single system. {\em Matita} is the result of this effort.
+
+At first sight, Matita looks as (and partly is) a Coq clone. This is
+more the effect of the circumstances of its creation described
+above than the result of a deliberate design. In particular, we
+(essentially) share the same foundational dialect of Coq (the
+Calculus of Inductive Constructions), the same implementative
+language (Ocaml), and the same (script based) authoring philosophy.
+However, as we shall see, the analogy essentially stops here.
+
+In a sense; we like to think of Matita as the way Coq would
+look like if entirely rerwritten from scratch: just to give an
+idea, although Matita currently supports almost all functionalities of
+Coq, it links 60000 lins of coaml code, against ... of Coq (and
+we are convinced that, starting from scratch againg, we could furtherly
+reduce our code in sensible way).
+
+
+\begin{itemize}
+ \item scelta del sistema fondazionale
+ \item sistema indipendente (da Coq)
+ \begin{itemize}
+ \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
+ implementative, \dots)
+ \item compatibilit\`a con sistemi legacy
+ \end{itemize}
+\end{itemize}
+
+\section{Features}
+
+\subsection{mathml}
+\ASSIGNEDTO{zack}
-{\bf Acknowledgements}
+\subsection{metavariabili}
+\ASSIGNEDTO{csc}
+
+\subsection{pattern}
+\ASSIGNEDTO{gares}
+
+\subsection{tatticali}
+\ASSIGNEDTO{gares}
+
+\subsection{disambiguazione}
+\ASSIGNEDTO{zack}
+
+\subsection{notazione}
+\ASSIGNEDTO{zack}
+
+\subsection{libreria tutta visibile}
+\ASSIGNEDTO{csc}
+
+\subsection{ricerca e indicizzazione}
+\ASSIGNEDTO{andrea}
+
+\subsection{auto}
+\ASSIGNEDTO{andrea}
+
+\subsection{xml / gestione della libreria}
+\ASSIGNEDTO{gares}
+
+\subsection{named variable}
+\ASSIGNEDTO{csc}
+
+\subsection{assenza di proof tree / resa in linguaggio naturale}
+\ASSIGNEDTO{andrea}
+
+\subsection{selezione semantica, cut paste, hyperlink}
+\ASSIGNEDTO{zack}
+
+\subsection{sostituzioni esplicite vs moduli}
+\ASSIGNEDTO{csc}
+
+\section{Drawbacks, missing, \dots}
+
+\subsection{moduli}
+\ASSIGNEDTO{}
+
+\subsection{ltac}
+\ASSIGNEDTO{}
+
+\subsection{estrazione}
+\ASSIGNEDTO{}
+
+\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
+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 / blobdiff