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 teps:
+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 for future system, where the documents
+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};
+ 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.
+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
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.
+to a set of software libraries, collectively called the \HELM{} libraries.
At the end of the \MOWGLI{} project we already disposed of the following
-techniques and libraries:
+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
partially specified terms, used by the disambiguating parser;
\item complex transformation algorithms for proof rendering in natural
language \cite{remathematization};
-\item an innovative rendering widget \cite{padovani}, supporting
+\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, the further step of developing our own
-proof assistant was too
-small and too tempting to be neglected. Essentially, we ``just'' had to
+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.
\TODO{alias one shot}
+\section{The logical library}
+Matita is Coq compatible, in the sense that every theorem of Coq
+can be read, checked and referenced in further developments.
+However, in order to test the actual usability of the system, a
+new library of results has been started from scratch. In this case,
+of course, the user may also dispose of the source script files,
+while in the case of Coq he may only rely on XML files of
+Coq objects.
+The current library just comprises about one thousand theorems in
+elementary aspects of arithmetics. The most complex result proved
+so far in Matita (that however, at our knoweledge, has never been proved
+before in any other system) is the multiplicative property for Eulers'
+totient function $\phi$.
+The library is organized in five main directories: $logic$ (connectives,
+quantifiers, equality, $\dots$), $datatypes$ (basic datatypes and type
+constructors), $nat$ (natural numbers), $Z$ (integers), $Q$ (rationals).
+The most complex development is $nat$, organized in 25 scripts, listed
+in Figure\ref{scripts}
+\begin{figure}[htb]
+$\begin{array}{lll}
+nat.ma & plus.ma & times.ma \\
+minus.ma & exp.ma & compare.ma \\
+orders.ma & le\_arith.ma & lt\_arith.ma \\
+factorial.ma & sigma\_and\_pi.ma & minimization.ma \\
+div\_and\_mod.ma & gcd.ma & congruence.ma \\
+primes.ma & nth\_prime.ma & ord.ma\\
+count.ma & relevant\_equations.ma & permutation.ma \\
+factorization.ma & chinese\_reminder.ma & fermat\_little\_th.ma \\
+totient.ma& & \\
+\end{array}$
+\caption{\label{scripts}Matita scripts on natural numbers}
+\end{figure}
+
+We do not plan to maintain the library in a centralized way,
+as most of the systems do. On the contary we are currently
+developing wiki-technologies to support a collaborative
+development of the library, encouraging people to expand,
+modify and elaborate previous contributions.
+
+
\acknowledgements
We would like to thank all the students that during the past
five years collaborated in the \HELM{} project and contributed to
projects / helm.git / commitdiff