snapshot

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

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

%\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{\IZ}{\ensuremath{\mathbb{Z}}}
\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{\NUPRL}{NuPRL}
\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}

\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
\newcommand{\URI}[1]{\texttt{#1}}

%{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
\newenvironment{grafite}{\VerbatimEnvironment
 \begin{SaveVerbatim}{boxtmp}}%
 {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
  \begin{center}
   \fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
  \end{center}}

\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
\newcommand{\FILE}[1]{\texttt{#1}}
\newcommand{\NOTE}[1]{\marginpar{\scriptsize #1}}
\newcommand{\TODO}[1]{\textbf{TODO: #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}}
\bibliographystyle{plain}

\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{mkm-helm} 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 35'000 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 \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-module},
has several major implications worth to be discussed. 

The first
point concerns the kind of content information to be exported. In a
proof assistant like \COQ{}, proofs are represented in at least three clearly
distinguishable formats: \emph{scripts} (i.e. sequences of commands issued by the
user to the system during an interactive session of proof), \emph{proof objects}
(which is the low-level representation of proofs in the form of
lambda-terms readable to and checked by kernel) and \emph{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 kernels of proof assistants 
often are). 
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 
(that 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 contractions 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 content into
a different text area.
\NOTE{il widget\\ non ha sel\\ semantica}
\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. \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 60'000 lins of \OCAML{} code, against ... of \COQ{} (and
we are convinced that, starting from scratch againg, we could furtherly
reduce our code in sensible way).\NOTE{righe\\\COQ{}}

\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}
\label{sec:metavariables}
\ASSIGNEDTO{csc}

\subsection{pattern}
\ASSIGNEDTO{gares}

\subsection{tatticali}
\ASSIGNEDTO{gares}

\subsection{Disambiguation}
\label{sec:disambiguation}
\ASSIGNEDTO{zack}

\begin{table}
 \caption{\label{tab:termsyn} Concrete syntax of CIC terms: built-in
 notation\strut}
\hrule
\[
\begin{array}{@{}rcll@{}}
  \NT{term} & ::= & & \mbox{\bf terms} \\
    &     & x & \mbox{(identifier)} \\
    &  |  & n & \mbox{(number)} \\
    &  |  & s & \mbox{(symbol)} \\
    &  |  & \mathrm{URI} & \mbox{(URI)} \\
    &  |  & \verb+_+ & \mbox{(implicit)}\TODO{sync} \\
    &  |  & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
    &  |  & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
    &  |  & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
    &  |  & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
    &  |  & \NT{term}~\NT{term} & \mbox{(application)} \\
    &  |  & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
    &  |  & \verb+match+~\NT{term}~ & \mbox{(pattern matching)} \\
    &     & ~ ~ [\verb+[+~\verb+in+~x~\verb+]+]
              ~ [\verb+[+~\verb+return+~\NT{term}~\verb+]+] \\
    &     & ~ ~ \verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \\
    &  |  & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
    &  |  & \verb+(+~\NT{term}~\verb+)+ \\
  \NT{defs}  & ::= & & \mbox{\bf mutual definitions} \\
    &     & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
  \NT{fun} & ::= & & \mbox{\bf functions} \\
    &     & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
  \NT{binder} & ::= & & \mbox{\bf binders} \\
    &     & \verb+\forall+ \mid \verb+\lambda+ \\
  \NT{arg} & ::= & & \mbox{\bf single argument} \\
    &     & \verb+_+ \mid x \\
  \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
    &     & \NT{arg} \\
    &  |  & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
  \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
    &     & \NT{arg} \\
    &  |  & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
  \NT{kind} & ::= & & \mbox{\bf induction kind} \\
    &     & \verb+rec+ \mid \verb+corec+ \\
  \NT{rule} & ::= & & \mbox{\bf rules} \\
    &     & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term}
\end{array}
\]
\hrule
\end{table}

\subsubsection{Term input}

The primary form of user interaction employed by \MATITA{} is textual script
editing: the user modifies it and evaluate step by step its composing
\emph{statements}. Examples of statements are inductive type definitions,
theorem declarations, LCF-style tacticals, and macros (e.g. \texttt{Check} can
be used to ask the system to refine a given term and pretty print the result).
Since many statements refer to terms of the underlying calculus, \MATITA{} needs
a concrete syntax able to encode terms of the Calculus of Inductive
Constructions.

Two of the requirements in the design of such a syntax are apparently in
contrast:
\begin{enumerate}
 \item the syntax should be as close as possible to common mathematical practice
  and implement widespread mathematical notations;
 \item each term described by the syntax should be non-ambiguous meaning that it
  should exists a function which associates to it a CIC term.
\end{enumerate}

These two requirements are addressed in \MATITA{} by the mean of two mechanisms
which work together: \emph{term disambiguation} and \emph{extensible notation}.
Their interaction is visible in the architecture of the \MATITA{} input phase,
depicted in Fig.~\ref{fig:inputphase}. The architecture is articulated as a
pipline of three levels: the concrete syntax level (level 0) is the one the user
has to deal with when inserting CIC terms; the abstract syntax level (level 2)
is an internal representation which intuitively encodes mathematical formulae at
the content level~\cite{adams}\cite{mkm-structure}; the last level is that of
CIC terms.

\begin{figure}[ht]
 \begin{center}
  \includegraphics[width=0.9\textwidth]{input_phase}
  \caption{\MATITA{} input phase}
 \end{center}
 \label{fig:inputphase}
\end{figure}

Requirement (1) is addressed by a built-in concrete syntax for terms, described
in Tab.~\ref{tab:termsyn}, and the extensible notation mechanisms which offers a
way for extending available mathematical notations. Extensible notation, which
is also in charge of providing a parsing function mapping concrete syntax terms
to content level terms, is described in Sect.~\ref{sec:notation}.  Requirement
(2) is addressed by the conjunct action of that parsing function and
disambiguation which provides a function from content level terms to CIC terms.

\subsubsection{Sources of ambiguity}

The translation from content level terms to CIC terms is not straightforward
because some nodes of the content encoding admit more that one CIC encoding,
invalidating requirement (2).

\begin{example}
 \label{ex:disambiguation}

 Consider the term at the concrete syntax level \texttt{\TEXMACRO{forall} x. x +
 ln 1 = x} of Fig.~\ref{fig:inputphase}(a), it can be the type of a lemma the
 user may want to prove. Assuming that both \texttt{+} and \texttt{=} are parsed
 as infix operators, all the following questions are legitimate and must be
 answered before obtaining a CIC term from its content level encoding
 (Fig.~\ref{fig:inputphase}(b)):

 \begin{enumerate}

  \item Since \texttt{ln} is an unbound identifier, which CIC constants does it
   represent? Many different theorems in the library may share its (rather
   short) name \dots

  \item Which kind of number (\IN, \IR, \dots) the \texttt{1} literal stand for?
   Which encoding is used in CIC to represent it? E.g., assuming $1\in\IN$, is
   it an unary or a binary encoding?

  \item Which kind of equality the ``='' node represents? Is it Leibniz's
   polymorhpic equality? Is it a decidable equality over \IN, \IR, \dots?

 \end{enumerate}

\end{example}

In \MATITA, three \emph{sources of ambiguity} are admitted for content level
terms: unbound identifiers, literal numbers, and operators. Each instance of
ambiguity sources (ambiguous entity) occuring in a content level term is
associated to a \emph{disambiguation domain}. Intuitively a disambiguation
domain is a set of CIC terms which may be replaced for an ambiguous entity
during disambiguation. Each item of the domain is said to be an
\emph{interpretation} for the ambiguous entity.

\emph{Unbound identifiers} (question 1) are ambiguous entities since the
namespace of CIC objects is not flat and the same identifier may denote many
ofthem. For example the short name \texttt{plus\_assoc} in the \HELM{} library
is shared by three different theorems stating the associative property of
different additions.  This kind of ambiguity is avoidable if the user is willing
to use long names (in form of URIs in the \texttt{cic://} scheme) in the
concrete syntax, with the obvious drawbacks of obtaining long and unreadable
terms.

Given an unbound identifier, the corresponding disambiguation domain is computed
querying the library for all constants, inductive types, and inductive type
constructors having it as their short name (see the \LOCATE{} query in
Sect.~\ref{sec:metadata}).

\emph{Literal numbers} (question 2) are ambiguous entities as well since
different kinds of numbers can be encoded in CIC (\IN, \IR, \IZ, \dots) using
different encodings. Considering the restricted example of natural numbers we
can for instance encode them in CIC using inductive datatypes with a number of
constructor equal to the encoding base plus 1, obtaining one encoding for each
base.

For each possible way of mapping a literal number to a CIC term, \MATITA{} is
aware of a \emph{number intepretation function} which, when applied to the
natural number denoted by the literal\footnote{at the moment only literal
natural number are supported in the concrete syntax} returns a corresponding CIC
term. The disambiguation domain for a given literal number is built applying to
the literal all available number interpretation functions in turn.

Number interpretation functions can be defined in OCaml or directly using
\TODO{notazione per i numeri}.

\emph{Operators} (question 3) are intuitively head of applications, as such they
are always applied to a non empty sequence of arguments. Their ambiguity is a
need since it is often the case that some notation is used in an overloaded
fashion to hide the use of different CIC constants which encodes similar
concepts. For example, in the standard library of \MATITA{} the infix \texttt{+}
notation is available building a binary \texttt{Op(+)} node, whose
disambiguation domain may refer to different constants like the addition over
natural numbers \URI{cic:/matita/nat/plus/plus.con} or that over real numbers of
the \COQ{} standard library \URI{cic:/Coq/Reals/Rdefinitions/Rplus.con}.

For each possible way of mapping an operator application to a CIC term,
\MATITA{} knows an \emph{operator interpretation function} which, when applied
to an operator and its arguments, returns a CIC term. The disambiguation domain
for a given operator is built applying to the operator and its arguments all
available operator interpretation functions in turn.

Operator interpretation functions could be added using the
\texttt{interpretation} statement. For example, among the first line of the
script \FILE{matita/library/logic/equality.ma} from the \MATITA{} standard
library we read:

\begin{grafite}
interpretation "leibnitz's equality"
 'eq x y =
   (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
\end{grafite}

Evaluating it in \MATITA{} will add an operator interpretation function for the
binary operator \texttt{eq} which expands to the CIC term on the right hand side
of the statement. That CIC term can be written using only built-in concrete
syntax, can contain no ambiguity source; still, it can refer to operator
arguments bound on the left hand side and can contain implicit terms (denoted
with \texttt{\_}) which will be expanded to fresh metavariables. The latter
feature is used in the example above for the first argument of Leibniz's
polymorhpic equality.

\subsubsection{Disambiguation algorithm}

\NOTE{assumo\\
      che si sia\\
      gia' parlato\\
      di refine}


A \emph{disambiguation algorithm} takes as input a content level term and return
a fully determined CIC term. The key observation on which a disambiguation
algorithm is based is that given a content level term with more than one sources
of ambiguity, not all possible combination of interpretation lead to a typable
CIC term. In the term of Ex.~\ref{ex:disambiguation} for instance the
interpretation of \texttt{ln} as a function from \IR to \IR and the
interpretation of \texttt{1} as the Peano number $1$ can't coexists. The notion
of ``can't coexists'' in the disambiguation of \MATITA{} is inherited from the
refiner described in Sect.~\ref{sec:metavariables}: as long as
$\mathit{refine}(c)\neq\bot$, the combination of interpretation which led to $c$
can coexists.

The \emph{naive disambiguation algorithm} takes as input a content level term
$t$ and proceeds as follows:

\begin{enumerate}

 \item Create disambiguation domains $\{D_i | i\in\mathit{Dom}(t)\}$, where
  $\mathit{Dom}(t)$ is the set of ambiguity sources of $t$. Each $D_i$ is a set
  of CIC terms and can be built as described above.

 \item Let $\Phi = \{\phi_i | {i\in\mathit{Dom}(t)},\phi_i\in D_i\}$ be an
  interpretation for $t$. Given $t$ and an interpretation $\Phi$, a CIC term is
  fully determined. Iterate over all possible interpretations of $t$ and refine
  the corresponding CIC terms, keep only interpretations which lead to CIC terms
  $c$ s.t. $\mathit{refine}(c)\neq\bot$ (i.e. interpretations that determine
  typable terms).

 \item Let $n$ be the number of interpretations who survived step 2. If $n=0$
  signal a type error. If $n=1$ we have found exactly one CIC term corresponding
  to $t$, returns it as output of the disambiguation phase. If $n>1$ we have
  found many different CIC terms which can correspond to the content level term,
  let the user choose one of the $n$ interpretations and returns the
  corresponding term.

\end{enumerate}

The above algorithm is highly inefficient since the number of possible
interpretations $\Phi$ grows exponentially with the number of ambiguity sources.
The actual algorithm used in \MATITA{} is far more efficient being, in the
average case, linear in the number of ambiguity sources.

\TODO{FINQUI}

The efficient algorithm can be applied if the logic can be extended with
metavariables and a refiner can be implemented. This is the case for CIC and
several other logics.
\emph{Metavariables}~\cite{munoz} are typed, non linear placeholders that can
occur in terms; $?_i$ usually denotes the $i$-th metavariable, while $?$ denotes
a freshly created metavariable. A \emph{refiner}~\cite{McBride} is a
function whose input is a term with placeholders and whose output is either a
new term obtained instantiating some placeholder or $\epsilon$, meaning that no
well typed instantiation could be found for the placeholders occurring in
the term (type error).

The efficient algorithm starts with an interpretation $\Phi_0 = \{\phi_i |
\phi_i = ?, i\in\mathit{Dom}(t)\}$,
which associates a fresh metavariable to each
source of ambiguity. Then it iterates refining the current CIC term (i.e. the
term obtained interpreting $t$ with $\Phi_i$). If the refinement succeeds the
next interpretation $\Phi_{i+1}$ will be created \emph{making a choice}, that is
replacing a placeholder with one of the possible choice from the corresponding
disambiguation domain. The placeholder to be replaced is chosen following a
preorder visit of the ambiguous term. If the refinement fails the current set of
choices cannot lead to a well-typed term and backtracking is attempted.
Once an unambiguous correct interpretation is found (i.e. $\Phi_i$ does no
longer contain any placeholder), backtracking is attempted
anyway to find the other correct interpretations.

The intuition which explain why this algorithm is more efficient is that as soon
as a term containing placeholders is not typable, no further instantiation of
its placeholders could lead to a typable term. For example, during the
disambiguation of user input \texttt{\TEXMACRO{forall} x. x*0 = 0}, an
interpretation $\Phi_i$ is encountered which associates $?$ to the instance
of \texttt{0} on the right, the real number $0$ to the instance of \texttt{0} on
the left, and the multiplication over natural numbers (\texttt{mult} for short)
to \texttt{*}. The refiner will fail, since \texttt{mult} require a natural
argument, and no further instantiation of the placeholder will be tried.

If, at the end of the disambiguation, more than one possible interpretations are
possible, the user will be asked to choose the intended one (see
Fig.~\ref{fig:disambiguation}).

\begin{figure}[htb]
%   \centerline{\includegraphics[width=0.9\textwidth]{disambiguation-1}}
  \caption{\label{fig:disambiguation} Disambiguation: interpretation choice}
\end{figure}

Details of the disambiguation algorithm of \WHELP{} can
be found in~\cite{disambiguation}, where an equivalent algorithm
that avoids backtracking is also presented.

\subsection{notazione}
\label{sec:notation}
\ASSIGNEDTO{zack}

\subsection{libreria tutta visibile}
\ASSIGNEDTO{csc}

\subsection{ricerca e indicizzazione}
\label{sec:metadata}
\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.

\bibliography{matita}

\end{document}