+The \components{} not yet described (\texttt{extlib}, \texttt{xml},
+\texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are
+minor \components{} that provide a core of useful functions and basic
+services missing from the standard library of the programming language.
+%In particular, the \texttt{xml} \component{} is used to easily represent,
+%parse and pretty-print XML files.
+
+
+\section{The interface to the library}
+
+A proof assistant provides both an interface to interact with its library and
+an \emph{authoring} interface to develop new proofs and theories. According
+to its historical origins, \MATITA{} strives to provide innovative
+functionalities for the interaction with the library. It is more traditional
+in its script based authoring interface.
+
+In the remaining part of the paper we focus on the user view of \MATITA{}.
+This section is devoted to the aspects of the tool that arise from the
+document centric approach to the library. Sect.~\ref{authoring} describes
+the peculiarities of the authoring interface.
+
+
+The library of \MATITA{} comprises mathematical concepts (theorems,
+axioms, definitions) and notation. The concepts are authored sequentially
+using scripts that are (ordered) sequences of procedural commands.
+However, once they are produced we store them independently in the library.
+The only relation implicitly kept between the notions are the logical,
+acyclic dependencies among them. This way the library forms a global (and
+distributed) hypertext. Several useful operations can be implemented on the
+library only, regardless of the scripts. Examples of such operations
+implemented in \MATITA{} are: searching and browing (see Sect.~\ref{sec:index});
+disambiguation of content level terms (see Sect.~\ref{sec:disambiguation});
+automatic proof searching (see Sect.~\ref{sec:automation}).
+
+A requisite for the previous operations is that the library must
+be fully accessible and in a logically consistent state. To preserve
+consistency, a concept cannot be altered or removed unless the part of the
+library that depends on it is modified accordingly. To allow incremental
+changes and cooperative development, consistent revisions are necessary.
+For instance, to modify a definition, the user could fork a new version
+of the library where the definition is updated and all the concepts that
+used to rely on it are absent. The user is then responsible to restore
+the removed part in the new branch, merging the branch when the library is
+fully restored.
+
+To implement the proposed versioning system on top of a standard one
+it is necessary to implement \emph{invalidation} first. Invalidation
+is the operation that locates and removes from the library all the concepts
+that depend on a given one. As described in Sect.~\ref{sec:...}, removing
+a concept from the library also involves deleting its metadata from the
+database.
+
+For non collaborative development, full versioning can be avoided, but
+invalidation is still required. Since nobody else is relying on your
+development, you are free to change and invalidate part of the library
+without branching. Invalidation is still necessary to avoid using a
+concept that is no longer valid.
+So far, in \MATITA{} we address only this non collaborative scenario
+(see Sect.~\ref{sec:decompilazione}). Collaborative development and versioning
+is still under design.
+
+Scripts are not seen as constituents of the library. They are not published
+and indexed, so they cannot be searched or browsed using \HELM{} tools.
+However, they play a central role for the mainteinance of the library.
+Indeed, once a notion is invalidated, the only way to restore it is to
+fix the possibly broken script that used to generate it.
+Moreover, during the authoring phase, scripts are a natural way to
+group notions together. They also constitute a less fine grained clustering
+of notions for invalidation.
+
+In the following sections we present in more details the functionalities
+of \MATITA{} related to library management and exploitation.
+
+
+
+\subsection{Indexing and searching}
+
+\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
+such an 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}
+Let's start with the definition of the ``strictly greater then'' notion over
+(Peano) natural numbers.
+
+\begin{grafite}
+include "nat/nat.ma".
+..
+definition gt: nat \to nat \to Prop \def
+ \lambda n, m. m < n.
+\end{grafite}
+
+The \texttt{include} statement adds the requirement that the part of the library
+defining the notion of natural numbers should be defined before
+processing the what follows. Note indeed that the algorithm presented
+in~\cite{disambiguation} does not describe where interpretations for ambiguous
+expressions come from, since it is application-specific. As a first
+approximation, we will assume that in \MATITA{} they come from the library (i.e.
+all interpretations available in the library are used) and the \texttt{include}
+statements are used to ensure the availability of required library slices (see
+Sect.~\ref{sec:libmanagement}).
+
+While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
+terms: its type and its body. Being available in the required library only one
+interpretation both for the unbound identifier \texttt{nat} and for the
+\OP{<} operator, and being the resulting partially specified term refinable,
+both type and body are easily disambiguated.
+
+Now suppose we have defined integers as signed natural numbers, and that we want
+to prove a theorem about an order relationship already defined on them (which of
+course overload the \OP{<} operator):
+
+\begin{grafite}
+include "Z/z.ma".
+..
+theorem Zlt_compat:
+ \forall x, y, z. x < y \to y < z \to x < z.
+\end{grafite}
+
+Since integers are defined on top of natural numbers, the part of the library
+concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
+type. Thus, according to the disambiguation algorithm, two different partially
+specified terms could be associated to it. At first, this might not be seen as a
+problem, since the user is asked and can choose interactively which of the two
+she had in mind. However in the long run it has the drawbacks of inhibiting
+batch compilation of the library (a technique used in \MATITA{} for behind the
+scene compilation when needed, e.g. when an \texttt{include} is issued) and
+yields to poor user interaction (imagine how tedious would be to be asked for a
+choice each time you re-evaluate \texttt{Zlt\_compat}!).
+
+For this reason we added to \MATITA{} the concept of \emph{disambiguation
+aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
+expressions to partially specified terms, which are part of the runtime status
+of \MATITA. They can be provided by users with the \texttt{alias} statement, but
+are usually automatically added when evaluating \texttt{include} statements
+(\emph{implicit aliases}). Aliases implicitely inferred during disambiguation
+are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
+which require interactive choice are saved in batch compilable format. Thus,
+after evaluating the above theorem the script will be changed to the following
+snippet (assuming that the interpretation of \OP{<} over integers has been
+choosed):
+
+\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}
+
+But how are disambiguation aliases used? Since they come from the parts of the
+library explicitely included we may be tempted of using them as the only
+available interpretations. This would speed up the disambiguation, but may fail.
+Consider for example:
+
+\begin{grafite}
+theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
+\end{grafite}
+
+and suppose that the \OP{+} operator is defined only on natural numbers. If
+the alias for \OP{<} points to the integer version of the operator, no
+refinable partially specified term matching the term could be found.
+
+For this reason we choosed to attempt \emph{multiple disambiguation passes}. A
+first pass attempt to disambiguate using the last available disambiguation
+aliases (\emph{mono aliases} pass), in case of failure the next pass try again
+the disambiguation forgetting the aliases and using the whole library to
+retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
+Since the latter pass may lead to too many choices we intertwined an additional
+pass among the two which use as interpretations all the aliases coming for
+included parts of the library (\emph{multi aliases} phase). This is the reason
+why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
+turned out to be a well-balanced trade-off among performances (earlier passes
+fail quickly) and degree of ambiguity supported for presentation level terms.
+
+\subsubsection{Operator instances}
+
+Let's suppose now we want to define a theorem relating ordering relations on
+natural and integer numbers. The way we would like to write such a theorem (as
+we can read it in the \MATITA{} standard library) is:
+
+\begin{grafite}
+include "Z/z.ma".
+include "nat/orders.ma".
+..
+theorem lt_to_Zlt_pos_pos:
+ \forall n, m: nat. n < m \to pos n < pos m.
+\end{grafite}
+
+Unfortunately, none of the passes described above is able to disambiguate its
+type, no matter how aliases are defined. 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 assign a different interpretation to each of
+them. A disambiguation pass which exploit this feature is said to be using
+\emph{fresh instances}.
+
+Fresh instances lead to a non negligible performance loss (since the choice of
+an interpretation for one instances does not constraint the choice for the
+others). For this reason we always attempt a fresh instances pass only after
+attempting a non-fresh one.
+
+\paragraph{One-shot aliases} Disambiguation aliases as seen so far are
+instance-independent. However, aliases obtained as a result of a disambiguation
+pass which uses fresh instances ought to be instance-dependent, that is: to
+ensure a term can be disambiguated in a batch fashion we may need to state that
+an \emph{i}-th instance of a symbol should be mapped to a given partially
+specified term. Instance-depend aliases are meaningful only for the term whose
+disambiguation generated it. For this reason we call them \emph{one-shot
+aliases} and \MATITA{} doesn't use it to disambiguate further terms down in the
+script.
+
+\subsubsection{Implicit coercions}
+
+Let's now consider a (rather hypothetical) theorem about derivation:
+
+\begin{grafite}
+theorem power_deriv:
+ \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
+\end{grafite}
+
+and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
+interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
+Mathematichians would write the term that way since it is well known that the
+natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
+number for the purpose of real multiplication. The refiner of \MATITA{} supports
+\emph{implicit coercions} for this reason: given as input the above content
+level term, it will return a partially specified term where in place of
+\texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
+(assuming it has been defined as such of course).
+
+Nonetheless coercions are not always desirable. For example, in disambiguating
+\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we don't want the term which uses
+two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
+among the possible partially specified term choices. For this reason in
+\MATITA{} we always try first a disambiguation pass which require the refiner
+not to use the coercions and only in case of failure we attempt a
+coercion-enabled pass.
+
+It is interesting to observe also the relationship among operator instances and
+implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
+which \MATITA{} disambiguated using fresh instances. In case there exists a
+coercion from natural numbers to (positive) integers (which indeed does, it is
+the \texttt{pos} constructor itself), the theorem can be disambiguated using
+twice that coercion on the left hand side of the implication. The obtained
+partially specified term however would not probably be the expected one, being a
+theorem which prove a trivial implication. For this reason we choose to always
+prefer fresh instances over implicit coercions, i.e. we always attempt
+disambiguation passes with fresh instances and no implicit coercions before
+attempting passes with implicit coercions.
+
+\subsubsection{Disambiguation passes}