Introduction (partial).

[helm.git] / helm / papers / matita / matita.tex

\documentclass[a4paper]{llncs}
\pagestyle{headings}
\usepackage{graphicx}
\usepackage{amssymb,amsmath}
\usepackage{hyperref}
\usepackage{picins}

%\newcommand{\logo}[3]{
%\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
%}

\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{\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}

\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\\
 Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY\\
 \email{$\{$asperti,sacerdot,tassi,zacchiro$\}$@cs.unibo.it}}

\begin{document}
\maketitle

\begin{abstract}
\end{abstract}

\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. 




\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}

\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 
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.
 \bibitem{pechino} A.Asperti, B.Wegner. \emph{An Approach to
  Machine-Understandable Representation of the Mathematical Information in
  Digital Documents}.  In: Fengshai Bai and Bernd Wegner (eds.): Electronic
  Information and Communication in Mathematics, LNCS vol. 2730, 
  pp. 14--23, 2003

 \bibitem{coq} The Coq proof-assistant, \url{http://coq.inria.fr}

 \bibitem{metadata1} F. Guidi, C. Sacerdoti Coen. \emph{Querying Distributed
  Digital Libraries of Mathematics}. In Proceedings of Calculemus 2003, 11th
  Symposium on the Integration of Symbolic Computation and Mechanized 
  Reasoning. Aracne Editrice.
 
 \bibitem{exportation} C. Sacerdoti Coen. \emph{From Proof-Assistans to
  Distributed Libraries of Mathematics: Tips and Pitfalls}.
  In Proc. Mathematical Knowledge Management 2003, Lecture Notes in Computer
  Science, Vol. 2594, pp. 30--44, Springer-Verlag.

 \bibitem{disambiguation} C. Sacerdoti Coen, S. Zacchiroli. \emph{Efficient
  Ambiguous Parsing of Mathematical Formulae}. In Proceedings of the Third
  International Conference on Mathematical Knowledge Management, MKM 2004. 
  LNCS,3119.

\end{thebibliography}

\end{document}