+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 minimize the need of
+user interaction during the disambiguation.
+
+\begin{table}[ht]
+ \caption{Disambiguation passes sequence\strut}
+ \label{tab:disambpasses}
+ \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\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}
+\end{table}
+
+\subsection{Generation and invalidation}
+\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 calculation of all the concepts that recursively
+depend on the ones we are invalidating. The calculation of the
+reverse dependencies can be computed using the relational database
+that stores metadata.
+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 script files 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.
+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
+disambiguation preferences declared or imported from other scripts
+(see \ref{sec:disambaliases}).
+
+Regenerating the content of a modified script file involves the preliminary
+invalidation of all its old content.
+
+\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 try 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 reexecute a
+whole script and similarly to invalidate the whole content of a script
+(together with all the other scripts that rely on an concept defined
+in it).
+
+\subsection{Automation}
+\label{sec:automation}
+
+\TODO{sezione sull'automazione}
+
+\subsection{Naming convention}
+\label{sec:naming}
+
+A minor but not entirely negligible aspect of \MATITA{} is that of
+adopting a (semi)-rigid naming convention for identifiers, derived by
+our studies about metadata for statements.
+The convention is only applied to identifiers for theorems
+(not definitions), and relates the name of a proof to its statement.
+The basic rules are the following:
+\begin{itemize}
+\item each identifier is composed by an ordered list of (short)
+names occurring in a left to right traversal of the statement;
+\item all identifiers should (but this is not strictly compulsory)
+separated by an underscore,
+\item identifiers in two different hypothesis, or in an hypothesis
+and in the conclusion must be separated by the string ``\verb+_to_+'';
+\item the identifier may be followed by a numerical suffix, or a
+single or double apostrophe.
+
+\end{itemize}
+Take for instance the theorem
+\[\forall n:nat. n = plus \; n\; O\]
+Possible legal names are: \verb+plus_n_O+, \verb+plus_O+,
+\verb+eq_n_plus_n_O+ and so on.
+Similarly, consider the theorem
+\[\forall n,m:nat. n<m \to n \leq m\]
+In this case \verb+lt_to_le+ is a legal name,
+while \verb+lt_le+ is not.\\
+But what about, say, the symmetric law of equality? Probably you would like
+to name such a theorem with something explicitly recalling symmetry.
+The correct approach,
+in this case, is the following. You should start with defining the
+symmetric property for relations
+
+\[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]
+
+Then, you may state the symmetry of equality as
+\[ \forall A:Type. symmetric \;A\;(eq \; A)\]
+and \verb+symmetric_eq+ is valid \MATITA{} name for such a theorem.
+So, somehow unexpectedly, the introduction of semi-rigid naming convention
+has an important beneficial effect on the global organization of the library,
+forcing the user to define abstract notions and properties before
+using them (and formalizing such use).
+
+Two cases have a special treatment. The first one concerns theorems whose
+conclusion is a (universally quantified) predicate variable, i.e.
+theorems of the shape
+$\forall P,\dots.P(t)$.
+In this case you may replace the conclusion with the word
+``elim'' or ``case''.
+For instance the name \verb+nat_elim2+ is a legal name for the double
+induction principle.
+
+The other special case is that of statements whose conclusion is a
+match expression.
+A typical example is the following
+\begin{verbatim}
+ \forall n,m:nat.
+ match (eqb n m) with
+ [ true \Rightarrow n = m
+ | false \Rightarrow n \neq m]
+\end{verbatim}
+where $eqb$ is boolean equality.
+In this cases, the name can be build starting from the matched
+expression and the suffix \verb+_to_Prop+. In the above example,
+\verb+eqb_to_Prop+ is accepted.
+
+\section{The authoring interface}
+\label{sec:authoring}
+
+The authoring interface of \MATITA{} is very similar to Proof General. We
+chose not to build the \MATITA{} UI over Proof General for two reasons. First
+of all we wanted to integrate our XML-based rendering technologies, mainly
+\GTKMATHVIEW. At the time of writing Proof General supports only text based
+rendering.\footnote{This may change with the future release of Proof General
+based on Eclipse, but is not yet the case.} The second reason is that we wanted
+to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
+as \GTK{} is.
+
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
+featuring two windows. The background one is very like to the Proof General
+interface. The main difference is that we use the \GTKMATHVIEW{} widget to
+render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
+advantage of the whole bidimensional mathematical notation. The foreground
+window is an instance of the cicBrowser used to render the proof being
+developed.
+
+Note that the syntax used in the script view is \TeX-like, however Unicode is
+fully supported so that mathematical glyphs can be input as such.
+
+\begin{figure}[!ht]
+ \begin{center}
+ \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
+ \caption{Authoring interface\strut}
+ \label{fig:screenshot}
+ \end{center}
+\end{figure}
+
+Since the concepts of script based proof authoring are well-known, the
+remaining part of this section is dedicated to the distinguishing
+features of the \MATITA{} authoring interface.
+
+\subsection{Direct manipulation of terms}
+\label{sec:directmanip}
+
+While terms are input as \TeX-like formulae in \MATITA, they are converted to a
+mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
+\GTKMATHVIEW. As described in~\cite{latexmathml} this mixed choice enables both
+high-quality bidimensional rendering of terms (including the use of fancy
+layout schemata like radicals and matrices) and the use of a
+concise and widespread textual syntax.
+
+Keeping pointers from the presentations level terms down to the
+partially specified ones \MATITA{} enable direct manipulation of
+rendered (sub)terms in the form of hyperlinks and semantic selection.
+
+\emph{Hyperlinks} have anchors on the occurrences of constant and
+inductive type constructors and point to the corresponding definitions
+in the library. Anchors are available notwithstanding the use of
+user-defined mathematical notation: as can be seen on the right of
+Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols
+encoding complex notations retain all the hyperlinks of constants or
+constructors used in the notation.
+
+\emph{Semantic selection} enables the selection of mixed
+\MATHML+\BOXML{} markup, constraining the selection to markup
+representing meaningful CIC (sub)terms. In the example on the left of
+Fig.~\ref{fig:directmanip} is thus possible to select the subterm
+$\mathrm{prime}~n$, whereas it would not be possible to select
+$\to n$ since the former denotes an application while the
+latter it not a subterm. Once a meaningful (sub)term has been
+selected actions can be done on it like reductions or tactic
+applications.
+
+\begin{figure}[!ht]
+ \begin{center}
+ \includegraphics[width=0.40\textwidth]{pics/matita-screenshot-selection}
+ \hspace{0.05\textwidth}
+ \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{pics/matita-screenshot-href}}
+ \caption[Semantic selection and hyperlinks]{Semantic selection (on the left)
+ and hyperlinks (on the right)\strut}
+ \label{fig:directmanip}
+ \end{center}
+\end{figure}