\newcommand{\MATITAC}{\texttt{matitac}}
\newcommand{\MATITADEP}{\texttt{matitadep}}
\newcommand{\MOWGLI}{MoWGLI}
+\newcommand{\MOWGLIIST}{IST-2001-33562}
\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
\newcommand{\NATIND}{\mathit{nat\_ind}}
\newcommand{\NUPRL}{NuPRL}
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
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
+European project \MOWGLIIST{} \MOWGLI~\cite{pechino}, mainly consisted in the
following steps:
\begin{itemize}
\item exporting the information from the internal representation of
\label{sec:indexing}
The \MATITA{} system is first of all an interface between the user and
-the mathematical repository. For this reason, it is important to be
-able to search and retrieve mathematical notions in a quick and
+the mathematical library. For this reason, it is important to be
+able to search and retrieve mathematical concepts in a quick and
effective way, assuming as little knowledge as possible about the
library. To this aim, \MATITA{} uses a sophisticated indexing mechanism
-for mathemtical items, based on a reach metadata set that has been
-tuned along the European Project IST-2001-33562 MoWGLI. The metadata
+for mathematical concepts, based on a rich metadata set that has been
+tuned along the European project \MOWGLIIST{} \MOWGLI. The metadata
set, and the searching facilites built on top of them --- collected
in the so called \WHELP{} search engine --- have been
extensively described in~\cite{whelp}. Let us just recall here that
\REF{p}{s}{t} stating that an object $s$ refers an object $t$ at a
given position $p$, where the position specify the place of the
occurrence of $t$ inside $s$ (we currently work with a fixed set of
-positions, discriminating, the hypothesis form the conclusion and
+positions, discriminating the hypothesis from the conclusion and
outermost form innermost occurrences). This approach is extremely
flexible, since extending the set of positions
we may improve the granularity and the precision of our indexing technique,
with no additional architectural impact.
-Every time a new mathematical object is created and saved by the user it gets
+Every time a new mathematical concept is created and saved by the user it gets
indexed, and becomes immediately visible in the library. Several
interesting and innovative features of \MATITA{} described in the following
sections rely in a direct or indirect way on its metadata system and
-the searching features. Here, we shall just recall some of its most
+the search features. Here, we shall just recall some of its most
direct applications.
A first, very simple but not negligeable feature is the check for duplicates.
-As soon as a new statement is defined, and before proving it,
+As soon as a theorem is stated, just before starting its proof,
the library is searched
to check that no other equivalent statement has been already proved
(based on the pattern matching functionality of \WHELP); if this is the case,
adopted by \MATITA{} is convertibility, but we may imagine to weaken it
in the future, covering for instance isomorphisms.
-Another usefull \WHELP{} operation is \HINT; we may invoke this query
-at any moment during the development of a proof, resulting in the list
+Another useful \WHELP{} operation is \HINT; we may invoke this query
+at any moment during the authoring of a proof, resulting in the list
of all theorems of the library which can be applied to the current
goal. In practice, this is mostly used not really to discover what theorems
can be applied to a given goal, but to actually retrieve a theorem that
we wish to apply, but whose name we have forgotten.
In fact, even if \MATITA{} adopts a semi-rigid naming convention for
-statements \ref{sec:naming} that greatly simplifies the effort of recalling
-names, the naming discipline remains one of the most
-annoying aspects of formal developments, and the hint feature provides
+statements (see Sect.~\ref{sec:naming}) that greatly simplifies the effort
+of recalling names, the naming discipline remains one of the most
+annoying aspects of formal developments, and \HINT{} provides
a very friendly solution.
In the near feature, we expect to extend the \HINT{} operation to
a \REWRITEHINT, resulting in all equational statements that
\TODO{conclusioni}
\acknowledgements
-We would like to thank all the students that during the past
-five years collaborated in the \HELM{} project and contributed to
+We would like to thank all the people that during the past
+7 years collaborated in the \HELM{} project and contributed to
the development of \MATITA{}, and in particular
M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
and V.~Tamburrelli.
\bibliography{matita}
\end{document}
-
projects / helm.git / commitdiff