+
+\section{Introduction}
+\label{sec:intro}
+\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 paper describes the overall architecture of
+the system, focusing on its most distintive and innovative
+features.
+
+\subsection{Historical Perspective}
+The origins of \MATITA{} go 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~\cite{CoqManual} 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{}\cite{nuprl-book}.
+The work, mostly performed in the framework of the recently concluded
+European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the
+following steps:
+\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\cite{content-centric} 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\footnote{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 software libraries, collectively called the \HELM{} libraries.
+At the end of the \MOWGLI{} project we already disposed of the following
+tools and software libraries:
+\begin{itemize}
+\item XML specifications for the Calculus of Inductive Constructions,
+with libraries for parsing and saving mathematical objects in such a format
+\cite{exportation-module};
+\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 \cite{remathematization};
+\item an innovative, MathML-compliant rendering widget for the GTK
+graphical environment\cite{padovani}, 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, developing our own proof assistant was not
+too far away: 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}
+DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
+
+\begin{itemize}
+ \item scelta del sistema fondazionale
+ \item sistema indipendente (da Coq)
+ \item compatibilit\`a con sistemi legacy
+\end{itemize}
+
+\subsection{Relationship with \COQ{}}
+
+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
+989 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 foster 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.
+