From 6f0e3275c5a100568c8529d6c58150ef4af692d0 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 30 Jan 2006 12:53:52 +0000 Subject: [PATCH] Draft of section Indexing and searching. --- helm/papers/matita/matita2.tex | 51 +++++++++++++++++++++++++++++++++- 1 file changed, 50 insertions(+), 1 deletion(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index e74021c5b..9dca4c677 100644 --- 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} -- 2.39.2