Draft of section Indexing and searching.

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index e74021c5b22c1c276693dc0c7139f1d780432737..9dca4c67768a9c5db5fdef044a3186be63d3a28e 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -756,8 +756,57 @@ the \MATITA{} authoring interface.
 
 \subsection{Indexing and searching}
 \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 
+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
+set, and the searching facilites built on top of them - collected 
+in the so called \whelp seach engine - have been
+extensively described in \cite{whelp}. Let us just recall here that
+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
+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 
+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
+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, 
+the library is searched 
+to check that no other equivalent statement has been already proved
+(based on the \whelp{} pattern matching functionality); if this is the case,
+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 {\em hint}; we may invoke this query
+at any moment during the development 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{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
+a very friendly solution.
+In the near feature, we expect to extend the {\em hint} operation to
+a {\em rewrite-hint}, resulting in all equational statements that
+can be applied to {\em rewrite} the current goal.
 
-\TODO{sezione sull'indicizzazione}
 
 \subsection{Disambiguation}
 \label{sec:disambiguation}