From: Stefano Zacchiroli Date: Mon, 30 Jan 2006 13:44:05 +0000 (+0000) Subject: uniformed terminology used in the indexing part to that used in the rest of the paper X-Git-Tag: make_still_working~7736 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2c8da9d687c102ab8bc4c0424080f64ff76f3c53;p=helm.git uniformed terminology used in the indexing part to that used in the rest of the paper --- diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index e1d283d69..81e0c1dee 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -30,6 +30,7 @@ \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} @@ -129,6 +130,7 @@ the system, focusing on its most distinctive 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 @@ -137,7 +139,7 @@ was chosen 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 +European project \MOWGLIIST{} \MOWGLI~\cite{pechino}, mainly consisted in the following steps: \begin{itemize} \item exporting the information from the internal representation of @@ -788,12 +790,12 @@ the \MATITA{} authoring interface. \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 @@ -801,21 +803,21 @@ the \WHELP{} metadata model is essentially based a single ternary relation \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, @@ -823,16 +825,16 @@ a warning is raised to the user. At present, the notion of equivalence 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 @@ -1779,8 +1781,8 @@ modify and elaborate previous contributions. \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. @@ -1790,4 +1792,3 @@ and V.~Tamburrelli. \bibliography{matita} \end{document} -