+\begin{figure}[!ht]
+ \begin{center}
+ \includegraphics[width=0.70\textwidth]{pics/cicbrowser-screenshot-con}
+ \caption[Natural language rendering]{Natural language rendering of a theorem
+ from the library\strut}
+ \label{fig:cicbrowser2}
+ \end{center}
+\end{figure}
+
+Several useful operations can be implemented on the library only,
+regardless of the scripts. For instance, searching and browsing is
+implemented by the ``cicBrowser'' window available from the \MATITA{}
+GUI. Using it, the hierarchical structure of the library can be
+explored (on the left of Fig.~\ref{fig:cicbrowser1}), the natural
+language rendering of proofs can be inspected
+(Fig.~\ref{fig:cicbrowser2}), and content based searches on the
+library can be performed (on the right of Fig.~\ref{fig:cicbrowser1}).
+Content based searches are described in
+Sect.~\ref{sec:indexing}. Other examples of library operations are
+disambiguation of content level terms (see
+Sect.~\ref{sec:disambiguation}) and automatic proof searching (see
+Sect.~\ref{sec:automation}).
+
+The key 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:libmanagement} 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 the
+user development, the user is 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:libmanagement}). 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 maintenance of the library.
+Indeed, once a concept 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 concepts together. They also constitute a less fine grained clustering
+of concepts for invalidation.
+
+In the rest of this section we present in more details the functionalities of
+\MATITA{} related to library management and exploitation.
+Sect.~\ref{sec:authoring} is devoted to the description of the peculiarities of
+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 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 facilities 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 on a single ternary relation
+\REF{p}{s}{t} stating that a concept $s$ refers a concept $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 functionalities. Here, we shall just recall some of its most
+direct applications.
+
+A first, very simple but not negligible feature is the \emph{duplicate check}.
+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~\cite{delahaye}.
+
+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 future, we expect to extend the \HINT{} query 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.
+The drift is still very large for
+proofs~\cite{debrujinfactor}, while better results may be achieved for
+mathematical formulae. In \MATITA{} formulae can be written using a
+\TeX-like 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 ingredient 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 detail 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 preferences}
+\label{sec:disambaliases}
+
+Consider the following command that states 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 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 explicitly given in the script (using the \texttt{alias}
+command), but
+are also implicitly added when a new concept is introduced (\emph{implicit
+preferences}) or after a successful 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 likelihood 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.
+The inclusion mechanism is thus sensibly different from that of other systems
+where concepts are effectively loaded and made visibible by inclusion; in \MATITA{}
+all concepts are always visible, and inclusion, that is optional, is only used
+to set up preferences.
+
+Preferences can be changed. For instance, at the beginning 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 restrictive 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 set of 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.
+
+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, where \texttt{pos} injects natural numbers
+into positive integers:
+
+\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,
+enabling the use of 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).
+
+Fresh instances lead to a non negligible performance loss (since the choice of
+an alias for one instance does not constraint the choice of the others). For
+this reason we always attempt a fresh instances pass only after attempting a
+shared instances pass.
+
+%\paragraph{One-shot preferences} Disambiguation preferences as seen so far are
+%instance-independent. However, implicit preferences obtained as a result of a
+%disambiguation pass which uses fresh instances ought to be instance-dependent.
+%Informally, the set of preferences that can be respected by the disambiguator on
+%the theorem above is: ``the first instance of the \OP{<} symbol is over natural
+%numbers, while the second is on integer numbers''.
+
+Instance-dependent preferences are meaningful only for the term whose
+disambiguation generated them. For this reason we call them \emph{one-shot
+preferences} and \MATITA{} does not use them to disambiguate further terms in
+the script.
+
+\subsubsection{Implicit coercions}
+\label{sec:disambcoercions}
+
+Consider the following theorem about derivation:
+\begin{grafite}
+theorem power_deriv:
+ \forall n: nat, x: R. d x^n dx = n * x^(n - 1).
+\end{grafite}
+and assume that in the library there is an alias mapping \OP{\^} to a partially
+specified term having type: \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}. In
+order to disambiguate \texttt{power\_deriv}, the occurrence of \texttt{n} on the
+right hand side of the equality need to be ``injected'' from \texttt{nat} to
+\texttt{R}. The refiner of \MATITA{} supports
+\emph{implicit coercions}~\cite{barthe95implicit} for
+this reason: given as input the above presentation 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 such a coercion has
+been defined in advance).
+
+Implicit coercions are not always desirable. For example, consider the term
+\texttt{\TEXMACRO{forall} x. x < x + 1} and assume that the preferences for \OP{<}
+and \OP{+} are over real numbers. The expected interpretation assignes the
+type \texttt{R} to \texttt{x}.
+However, if we had a coercion from natural to real numbers an alternative
+interpretation is to assign the type \texttt{nat} to \texttt{x} inserting the coercion
+as needed. Clearly, the latter interpretation looks artificial and
+for this reason we enable coercions only in case of failure of previous
+attempts.
+
+The choice of whether implicit coercions are enabled or not interacts with the
+choice about operator instances. Indeed, consider again
+\texttt{lt\_to\_Zlt\_pos\_pos}, which can be disambiguated using fresh operator
+instances. In case there exists a coercion from natural numbers to positive
+integers ({\texttt{pos} itself), the command
+can be disambiguated as
+\texttt{\TEXMACRO{forall} n,m: nat. pos n < pos m \TEXMACRO{to} pos n < pos m}.
+This is not the expected interpretation;
+by this and similar examples we choose to always prefer fresh
+instances over implicit coercions.
+
+\subsubsection{Disambiguation passes}
+\label{sec:disambpasses}
+
+According to the criteria described above, in \MATITA{} we perform the
+disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
+our experience that choice gives reasonable performance and reduces the need
+of user interaction during the disambiguation.
+
+\begin{table}[ht]
+ \begin{center}
+ \begin{tabular}{c|c|c|c}
+ \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
+ & \multicolumn{1}{p{3.1cm}|}{\centering\raisebox{-1.5ex}{\textbf{Preferences}}}
+ & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
+ & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
+ \hline
+ \PASS & Mono-preferences & Shared instances & Disabled \\
+ \PASS & Multi-preferences & Shared instances & Disabled \\
+ \PASS & Mono-preferences & Fresh instances & Disabled \\
+ \PASS & Multi-preferences & Fresh instances & Disabled \\
+ \PASS & Mono-preferences & Fresh instances & Enabled \\
+ \PASS & Multi-preferences & Fresh instances & Enabled \\
+ \PASS & Library-preferences & Fresh instances & Enabled
+ \end{tabular}
+ \end{center}
+ \caption{Disambiguation passes sequence\strut}
+ \label{tab:disambpasses}
+\end{table}
+
+\subsection{Invalidation and regeneration}
+\label{sec:libmanagement}
+
+%The aim of this section is to describe the way \MATITA{}
+%preserves the consistency and the availability of the library
+%using the \WHELP{} technology, in response to the user alteration or
+%removal of mathematical objects.
+%
+%As already sketched in Sect.~\ref{sec:fullyintro} what we generate
+%from a script is split among two storage media, a
+%classical filesystem and a relational database. The former is used to
+%store the XML encoding of the objects defined in the script, the
+%disambiguation aliases and the interpretation and notational convention defined,
+%while the latter is used to store all the metadata needed by
+%\WHELP.
+%
+%While the consistency of the data store in the two media has
+%nothing to do with the nature of
+%the content of the library and is thus uninteresting (but really
+%tedious to implement and keep bug-free), there is a deeper
+%notion of mathematical consistency we need to provide. Each object
+%must reference only defined object (i.e. each proof must use only
+%already proved theorems).
+
+In this section we will focus on how \MATITA{} ensures the library
+consistency during the formalization of a mathematical theory,
+giving the user the freedom of adding, removing, modifying objects
+without loosing the feeling of an always visible and browsable
+library.
+
+\subsubsection{Invalidation}
+
+Invalidation (see Sect.~\ref{sec:library}) is implemented in two phases.
+
+The first one is the computation of all the concepts that recursively
+depend on the ones we are invalidating. It can be performed
+from the metadata stored in the relational database.
+This technique is the same used by the \emph{Dependency Analyzer}
+and is described in~\cite{zack-master}.
+
+The second phase is the removal of all the results of the generation,
+metadata included.
+
+\subsubsection{Regeneration}
+
+%The typechecker component guarantees that if an object is well typed
+%it depends only on well typed objects available in the library,
+%that is exactly what we need to be sure that the logic consistency of
+%the library is preserved.
+
+To regenerate an invalidated part of the library \MATITA{} re-executes
+the scripts that produced the invalidated concepts. The main
+problem is to find a suitable order of execution of the scripts.
+
+For this purpose we provide a tool called \MATITADEP{}
+that takes in input the list of scripts that compose the development and
+outputs their dependencies in a format suitable for the GNU \texttt{make}
+tool.\footnote{\url{http://www.gnu.org/software/make/}}
+The user is not asked to run \MATITADEP{} by hand, but
+simply to tell \MATITA{} the root directory of his development (where all
+script files can be found) and \MATITA{} will handle all the generation
+related tasks, including dependencies calculation.
+
+To compute dependencies it is enough to look at the script files for
+literal of included explicit disambiguation preferences
+(see Sect.~\ref{sec:disambaliases}).
+
+The re-execution of a script to regenerate part of the library
+requires the preliminary invalidation of the concepts generated by the
+script.
+
+\subsubsection{Batch vs Interactive}
+
+\MATITA{} includes an interactive authoring interface and a batch
+``compiler'' (\MATITAC).
+
+Only the former is intended to be used directly by the
+user, the latter is automatically invoked by \MATITA{}
+to regenerate parts of the library previously invalidated.
+
+While they share the same engine for generation and invalidation, they
+provide different granularity. \MATITAC{} is only able to re-execute a
+whole script and similarly to invalidate all the concepts generated
+by a script (together with all the other scripts that rely on a concept defined
+in it).
+
+\subsection{Automation}
+\label{sec:automation}
+
+In the long run, one would expect to work with a proof assistant
+like \MATITA, using only three basic tactics: \TAC{intro}, \TAC{elim},
+and \TAC{auto}
+(possibly integrated by a moderate use of \TAC{cut}). The state of the art
+in automated deduction is still far away from this goal, but
+this is one of the main development direction of \MATITA.
+
+Even in this field, the underlying philosophy of \MATITA{} is to
+free the user from any burden relative to the overall management
+of the library. For instance, in \COQ, the user is responsible to
+define small collections of theorems to be used as a parameter
+by the \TAC{auto} tactic;
+in \MATITA, it is the system itself that automatically retrieves, from
+the whole library, a subset of theorems worth to be considered
+according to the signature of the current goal and context.
+
+The basic tactic merely iterates the use of the \TAC{apply} tactic
+(with no \TAC{intro}). The search tree may be pruned according to two
+main parameters: the \emph{depth} (whit the obvious meaning), and the
+\emph{width} that is the maximum number of (new) open goals allowed at
+any instant. \MATITA{} has only one notion of metavariable, corresponding
+to the so called existential variables of \COQ; so, \MATITA's \TAC{auto}
+tactic should be compared with \COQ's \TAC{EAuto} tactic.
+
+Recently we have extended automation with paramodulation based
+techniques. At present, the system works reasonably well with
+equational rewriting, where the notion of equality is parametric
+and can be specified by the user: the system only requires
+a proof of {\em reflexivity} and {\em paramodulation} (or rewriting,
+as it is usually called in the proof assistant community).
+
+Given an equational goal, \MATITA{} recovers all known equational facts
+from the library (and the local context), applying a variant of
+the so called {\em given-clause algorithm}~\cite{paramodulation},
+that is the the procedure currently used by the majority of modern
+automatic theorem provers.
+
+The given-clause algorithm is essentially composed by an alternation
+of a \emph{saturation} phase and a \emph{demodulation} phase.
+The former derives new facts by a set of active
+facts and a new \emph{given} clause suitably selected from a set of passive
+equations. The latter tries to simplify the equations
+orienting them according to a suitable weight associated to terms.
+\MATITA{} currently supports several different weighting functions
+comprising Knuth-Bendix ordering (kbo) and recursive path ordering (rpo),
+that integrates particularly well with normalization.
+
+Demodulation alone is already a quite powerful technique, and
+it has been turned into a tactic by itself: the \TAC{demodulate}
+tactic, which can be seen as a kind of generalization of \TAC{simplify}.
+The following portion of script describes two
+interesting cases of application of this tactic (both of them relying
+on elementary arithmetic equations):
+
+\begin{grafite}
+theorem example1:
+ \forall x: nat. (x+1)*(x-1) = x*x - 1.
+intro.
+apply (nat_case x);
+ [ simplify; reflexivity
+ | intro; demodulate; reflexivity ]
+qed.
+\end{grafite}