\end{opening}
+\section{Introduction}
+\label{sec:intro}
+In this paper we describe the architecture and a few distintive features of the
+\emph{\MATITA} proof assistant. \MATITA{} was not conceived out of the blue
+one single day; it has been the next natural step in the evolution of one
+line of research we started six years ago. Thus, to better understand the
+system, we start from its historical roots.
+
+\subsection{Historical Perspective}
+\MATITA{} is 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-centric 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}
+
+According to our content-centric commitment, the library exported from
+Coq was conceived as being distributed and most of the tools were developed
+as Web services. The user could interact with the library and the tools by
+means of a Web interface that orchestrates the Web services.
+
+The Web services and the other tools have been implemented as front-ends
+to a set of libraries, collectively called the \HELM{} libraries.
+At the end of the \MOWGLI{} project we already disposed of the following
+techniques and libraries:
+\begin{itemize}
+\item XML specifications for the Calculus of Inductive Constructions,
+with libraries for parsing and saving mathematical objects in such a format;
+\item metadata specifications with libraries for indexing and querying the
+XML knowledge base;
+\item a proof checker library (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{disambiguation};
+\item a {\em refiner} library, i.e. a type inference system, based on
+partially specified terms, 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
+meaningful rendering expressions, and to past the respective content 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. \MATITA{} is the result of this effort.
+
+\subsection{The System}
+
+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 (Co)Inductive Constructions), the same implementative
+language (\OCAML{}), and the same (script based) authoring philosophy.
+However, the analogy essentially stops here and no code is shared by the
+two systems.
+
+In a sense; we like to think of \MATITA{} as the way \COQ{} would
+look like if entirely rewritten from scratch: just to give an
+idea, although \MATITA{} currently supports almost all functionalities of
+\COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked
+by \COQ{} (and we are convinced that, starting from scratch again,
+we could furtherly reduce our code in sensible way).
+
+Moreover, the complexity of the code of \MATITA{} is greatly reduced with
+respect to \COQ. For instance, the API of the libraries of \MATITA{} comprise
+916 functions, to be compared with the 4'286 functions of \COQ.
+
+Finally, \MATITA{} has several innovatives features over \COQ{} that derive
+from the integration of Mathematical Knowledge Management tools with proof
+assistants. Among them, the advanced indexing tools over the library and
+the parser for ambiguous mathematical notation.
+
+The size and complexity improvements over \COQ{} must be understood
+historically. \COQ{} is a quite old
+system whose development started 15\NOTE{Verificare} years ago. Since then
+several developers have took over the code and several new research ideas
+that were not considered in the original architecture have been experimented
+and integrated in the system. Moreover, there exists a lot of developments
+for \COQ{} that require backward compatibility between each pair of releases;
+since many central functionalities of a proof assistant are based on heuristics
+or arbitrary choices to overcome undecidability (e.g. for higher order
+unification), changing these functionalities mantaining backward compatibility
+is very difficult. Finally, the code of \COQ{} has been greatly optimized
+over the years; optimization reduces maintenability and rises the complexity
+of the code.
+
+In writing \MATITA{} we have not been hindered by backward compatibility and
+we have took advantage of the research results and experiences previously
+developed by others, comprising the authors of \COQ. Moreover, starting from
+scratch, we have designed in advance the architecture and we have splitted
+the code in coherent minimally coupled libraries.
+
+In the future we plan to exploit \MATITA{} as a test bench for new ideas and
+extensions. Keeping the single libraries and the whole architecture as
+simple as possible is thus crucial to speed up future experiments and to
+allow other developers to quickly understand our code and contribute.
+For direct experience of the authors, the learning curve to understand and
+be able to contribute to \COQ{}'s code is quite steep and requires direct
+and frequent interactions with \COQ{} developers.
+
+\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}
+
\begin{figure}[t]
\begin{center}
\includegraphics[width=0.9\textwidth]{librariesCluster.ps}
- \caption{\MATITA{} libraries}
+ \caption{\label{fig:libraries}\MATITA{} libraries}
\end{center}
- \label{fig:libraries}
\end{figure}
\section{Overview of the Architecture}
projects / helm.git / commitdiff