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}