+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.
+