+\label{sec:indexing}
+
+The \MATITA{} system is first of all an interface between the user 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 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
+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 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 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 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 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,
+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 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 (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
+can be applied to rewrite the current goal.
+
+\subsection{Disambiguation}
+\label{sec:disambiguation}
+
+Software applications that involve input of mathematical content should strive
+to require the user as less drift from informal mathematics as possible. We
+believe this to be a fundamental aspect of such applications user interfaces.
+Being that drift in general very large when inputing
+proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
+mathematical formulae which can be input using a \TeX-like encoding (the
+concrete syntax corresponding to presentation level terms) and are then
+translated (in multiple steps) to partially specified terms as sketched in
+Sect.~\ref{sec:contentintro}.
+
+The key component of the translation is the generic disambiguation algorithm
+implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
+and presented in~\cite{disambiguation}. In this section we present how to use
+that algorithm in the context of the development of a library of formalized
+mathematics. We will see that using multiple passes of the algorithm, varying
+some of its parameters, helps in keeping the input terse without sacrificing
+expressiveness.
+
+\subsubsection{Disambiguation aliases}
+\label{sec:disambaliases}
+
+Consider the following command to state a theorem over integer numbers:
+
+\begin{grafite}
+theorem Zlt_compat:
+ \forall x, y, z. x < y \to y < z \to x < z.
+\end{grafite}
+
+The symbol \OP{<} is likely to be overloaded in the library
+(at least over natural numbers).
+Thus, according to the disambiguation algorithm, two different
+refinable partially specified terms could be associated to it.
+\MATITA{} asks the user what interpretation he meant. However, to avoid
+posing the same question in case of a future re-execution (e.g. undo/redo),
+the choice must be recorded. Since scripts need to be re-executed after
+invalidation, the choice record must be permanently stored somewhere. The most
+natural place is in the script itself.
+
+In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}.
+They are mappings, stored in the library, from ambiguity sources
+(identifiers, symbols and literal numbers at the content level) to partially
+specified terms. In case of overloaded sources there exists multiple aliases
+with the same source. It is possible to record \emph{disambiguation
+preferences} to select one of the aliases of an overloaded source.
+
+Preferences can be explicitely given in the script (using the
+misleading \texttt{alias} commands), but
+are also implicitly added when a new concept is introduced (\emph{implicit
+preferences}) or after a sucessfull disambiguation that did not require
+user interaction. Explicit preferences are added automatically by \MATITA{} to
+record the disambiguation choices of the user. For instance, after the
+disambiguation of the command above, the script is altered as follows:
+
+\begin{grafite}
+alias symbol "lt" = "integer 'less than'".
+theorem Zlt_compat:
+ \forall x, y, z. x < y \to y < z \to x < z.
+\end{grafite}
+
+The ``alias'' command in the example sets the preferred alias for the
+\OP{lt} symbol.
+
+Implicit preferences for new concepts are set since a concept just defined is
+likely to be the preferred one in the rest of the script. Implicit preferences
+learned from disambiguation of previous commands grant the coherence of
+the disambiguation in the rest of the script and speed up disambiguation
+reducing the search space.
+
+Disambiguation preferences are included in the lexicon status
+(see Sect.~\ref{sec:presentationintro}) that is part of the authoring interface
+status. Unlike aliases, they are not part of the library.
+
+When starting a new authoring session the set of disambiguation preferences
+is empty. Until it contains a preference for each overloaded symbol to be
+used in the script, the user can be faced with questions from the disambiguator.
+To reduce the likelyhood of user interactions, we introduced
+the \texttt{include} command. With \texttt{include} it is possible to import
+at once in the current session the set of preferences that was in effect
+at the end of the execution of a given script.
+
+Preferences can be changed. For instance, at the start of the development
+of integer numbers the preference for the symbol \OP{<} is likely
+to be the one over natural numbers; sooner or later it will be set to the one
+over integer numbers.
+
+Nothing forbids the set of preferences to become incoherent. For this reason
+the disambiguator cannot always respect the user preferences.
+Consider, for example:
+\begin{grafite}
+theorem Zlt_mono:
+ \forall x, y, k. x < y \to x < y + k.
+\end{grafite}
+
+No refinable partially specified term corresponds to the preferences:
+\OP{+} over natural numbers, \OP{<} over integer numbers. To overcome this
+limitation we organized disambiguation in \emph{multiple passes}: when the
+disambiguator fails, disambiguation is tried again with a less strict set of
+preferences.
+
+Several disambiguation parameters can vary among passes. With respect to
+preference handling we implemented three passes. In the first pass, called
+\emph{mono-preferences}, we consider only the aliases corresponding to the
+current preferences. In the second pass, called \emph{multi-preferences}, we
+consider every alias corresponding to a current or past preference. For
+instance, in the example above disambiguation succeeds in the multi-preference
+pass. In the third pass, called \emph{library-preferences}, all aliases
+available in the library are considered.
+
+\TODO{rivedere questo periodo\ldots}
+The rationale behind this choice is trying to respect user preferences in early
+passes that complete quickly in case of failure; later passes are slower but
+have more chances of success.
+
+\subsubsection{Operator instances}
+\label{sec:disambinstances}
+
+Consider now the following theorem:
+\begin{grafite}
+theorem lt_to_Zlt_pos_pos:
+ \forall n, m: nat. n < m \to pos n < pos m.
+\end{grafite}
+and assume that there exist in the library aliases for \OP{<} over natural
+numbers and over integer numbers. None of the passes described above is able to
+disambiguate \texttt{lt\_to\_Zlt\_pos\_pos}, no matter how preferences are set.
+This is because the \OP{<} operator occurs twice in the content level term (it
+has two \emph{instances}) and two different interpretations for it have to be
+used in order to obtain a refinable partially specified term.
+
+To address this issue, we have the ability to consider each instance of a single
+symbol as a different ambiguous expression in the content level term, and thus
+we can use a different alias for each of them. Exploiting or not this feature is
+one of the disambiguation pass parameters. A disambiguation pass which exploit
+it is said to be using \emph{fresh instances} (opposed to a \emph{shared
+instances} pass).