+\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}
+
+\begin{grafite}
+theorem example2:
+ \forall x,y: nat. (x+y)*(x+y) = x*x + 2*x*y + y*y.
+intros; demodulate; reflexivity
+qed.
+\end{grafite}
+
+In the future we expect to integrate applicative and equational
+rewriting. In particular, the overall idea would be to integrate
+applicative rewriting with demodulation, treating saturation as an
+operation to be performed in batch mode, e.g. during the night.
+
+\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 concept names, derived by
+our studies about metadata for statements.
+The convention is only applied to theorems
+(not definitions), and relates theorem names to their statements.
+The basic rules are the following:
+\begin{itemize}
+
+ \item each name is composed by an ordered list of (short)
+ identifiers occurring in a left to right traversal of the statement;
+
+ \item all names should (but this is not strictly compulsory)
+ separated by an underscore;
+
+ \item names occurring in two different hypotheses, or in an hypothesis
+ and in the conclusion must be separated by the string \texttt{\_to\_};
+
+ \item the identifier may be followed by a numerical suffix, or a
+ single or double apostrophe.
+
+\end{itemize}
+
+Take for instance the statement:
+\begin{grafite}
+\forall n: nat. n = plus n O
+\end{grafite}
+Possible legal names are: \texttt{plus\_n\_O}, \texttt{plus\_O},
+\texttt{eq\_n\_plus\_n\_O} and so on.
+
+Similarly, consider the statement
+\begin{grafite}
+\forall n,m: nat. n < m to n \leq m
+\end{grafite}
+In this case \texttt{lt\_to\_le} is a legal name,
+while \texttt{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:
+\begin{grafite}
+definition symmetric \def
+ \lambda A: Type. \lambda R. \forall x,y: A.
+ R x y \to R y x.
+\end{grafite}
+Then, you may state the symmetry of equality as:
+\begin{grafite}
+\forall A: Type. symmetric A (eq A)
+\end{grafite}
+and \texttt{symmetric\_eq} is a legal 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 concepts 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 string
+\texttt{elim} or \texttt{case}.
+For instance the name \texttt{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{grafite}
+\forall n,m: nat.
+ match (eqb n m) with
+ [ true \Rightarrow n = m
+ | false \Rightarrow n \neq m ]
+\end{grafite}
+where \texttt{eqb} is boolean equality.
+In this cases, the name can be build starting from the matched
+expression and the suffix \texttt{\_to\_Prop}. In the above example,
+\texttt{eqb\_to\_Prop} is accepted.
+
+\section{The authoring interface}
+\label{sec:authoring}
+
+The authoring interface of \MATITA{} is very similar to Proof
+General~\cite{proofgeneral}. We
+chose not to build the \MATITA{} UI over Proof General for two reasons. First
+of all we wanted to integrate in the UI our rendering technologies, mainly
+\GTKMATHVIEW, to render sequents exploiting the bidimensional mathematical layouts
+of \MATHML-Presentation.
+At the time of writing Proof General supports only text based
+rendering.\footnote{This may change with future releases of Proof General
+based on Eclipse (\url{http://www.eclipse.org/}).} The second reason is that we wanted
+to build the \MATITA{} UI on top of a state-of-the-art and widespread graphical
+toolkit as \GTK{} is.
+
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface.
+The foreground
+window is an instance of the cicBrowser (see Sect.~\ref{sec:library}) used to
+render in natural language the proof under development.
+
+Note that the syntax used in the script view is \TeX-like, but
+Unicode\footnote{\url{http://www.unicode.org/}} is
+also 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 devoted 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{} enables 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 $\nmid$, 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 is not a subterm. Once a meaningful (sub)term has been
+selected actions like reductions or tactic applications can be performed on it.
+
+\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}
+
+\subsection{Patterns}
+\label{sec:patterns}
+
+In several situations working with direct manipulation of terms is
+simpler and faster than typing the corresponding textual
+commands~\cite{proof-by-pointing}.
+Nonetheless we need to record actions and selections in scripts.
+
+In \MATITA{} \emph{patterns} are textual representations of selections.
+Users can select using the GUI and then ask the system to paste the
+corresponding pattern in this script. More often this process is
+transparent to the user: once an action is performed on a selection,
+the corresponding
+textual command is computed and inserted in the script.
+
+\subsubsection{Pattern syntax}
+
+Patterns are composed of two parts: \NT{sequent\_path} and
+\NT{wanted}; their concrete syntax is reported in Tab.~\ref{tab:pathsyn}.
+
+\NT{sequent\_path} mocks-up a sequent, discharging unwanted subterms
+with \OP{?} and selecting the interesting parts with the placeholder
+\OP{\%}. \NT{wanted} is a term that lives in the context of the
+placeholders.
+
+Textual patterns produced from a graphical selection are made of the
+\NT{sequent\_path} only. Such patterns can represent every selection,
+but are quite verbose. The \NT{wanted} part of the syntax is meant to
+help the users in writing concise and elegant patterns by hand.
+
+\begin{table}
+ \caption{Patterns concrete syntax\strut}
+ \label{tab:pathsyn}
+\hrule
+\[
+\begin{array}{@{}rcll@{}}
+ \NT{pattern} &
+ ::= & [~\verb+in+~\NT{sequent\_path}~]~[~\verb+match+~\NT{wanted}~] & \\
+ \NT{sequent\_path} &
+ ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
+ [~\verb+\vdash+~\NT{multipath}~] & \\
+ \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
+ \NT{wanted} & ::= & \NT{term} & \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\subsubsection{Pattern evaluation}
+
+Patterns are evaluated in two phases. The first selects roots
+(subterms) of the sequent, using the \NT{sequent\_path}, while the
+second searches the \NT{wanted} term starting from that roots.
+% Both are optional steps, and by convention the empty pattern selects
+% the whole conclusion.
+
+\begin{description}
+\item[Phase 1]
+ concerns only \NT{sequent\_path}. \NT{ident} is an hypothesis name and selects
+ the assumption where the following optional \NT{multipath} will operate.
+ \verb+\vdash+ can be considered the name for the goal. If the whole pattern
+ is omitted, the whole goal will be selected. If one or more hypothesis names
+ are given, the selection is restricted to that assumptions. If a
+ $\NT{multipath}$ is omitted the whole assumption is selected. Remember that
+ the user can be mostly unaware of patterns concrete syntax, since the system
+ is able to write down a \NT{sequent\_path} starting from a graphical
+ selection.
+
+ A \NT{multipath} is a CIC term in which a special constant \OP{\%} is allowed.
+ The roots of discharged subterms are marked with \OP{?}, while \OP{\%} is used
+ to select roots. The default \NT{multipath}, the one that selects the whole
+ term, is simply \OP{\%}. Valid \NT{multipath} are, for example, \texttt{(? \%
+ ?)} or \texttt{\% \TEXMACRO{to} (\% ?)} that respectively select the first
+ argument of an application or the source of an arrow and the head of the
+ application that is found in the arrow target.
+
+ This phase not only selects terms (roots of subterms) but determines also
+ their context that will be possibly used in the next phase.
+
+\item[Phase 2]
+ plays a role only if \NT{wanted} is specified. From the first phase we
+ have some terms, that we will use as roots, and their context.
+ For each of these contexts the \NT{wanted} term is disambiguated in it
+ and the corresponding root is searched for a subterm that can be unified to
+ \NT{wanted}. The result of this search is the selection the
+ pattern represents.
+
+\end{description}
+
+\subsubsection{Examples}
+
+Consider the following sequent:
+\sequent{n: nat\\m: nat\\H: m + n = n}{m = O}
+
+To change the right part of the equality of the $H$
+hypothesis with $O + n$, the user selects and pastes it as the pattern
+in the following statement.
+\begin{grafite}
+ change in H:(? ? ? %) with (O + n).
+\end{grafite}
+
+To understand the pattern (or produce it by hand) the user should be aware that
+the notation $m + n = n$ hides the term $\mathrm{eq}~\mathrm{nat}~(m + n)~n$, so
+that the pattern selects only the third argument of $\mathrm{eq}$.
+
+The experienced user may also write by hand a concise pattern to change at once
+all the occurrences of $n$ in the hypothesis $H$:
+\begin{grafite}
+ change in H match n with (O + n).
+\end{grafite}
+
+In this case the \NT{sequent\_path} selects the whole $H$, while
+the second phase locates $n$.
+
+The latter pattern is equivalent to the following one, that the system
+can automatically generate from the selection.
+\begin{grafite}
+ change in H:(? ? (? ? %) %) with (O + n).
+\end{grafite}
+
+\subsubsection{Comparison with \COQ{}}
+
+In \MATITA{} all the tactics that act on subterms of the current sequent
+accept pattern arguments. Additional arguments can be disambiguated in the
+contexts of the terms selected by the pattern
+(\emph{context-dependent arguments}).
+
+%\NOTE{attualmente rewrite e fold non supportano fase 2. per
+%supportarlo bisogna far loro trasformare il pattern phase1+phase2
+%in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
+%con una pattern\_of(select(pattern))}
+
+\COQ{} has two different ways of restricting the application of tactics to
+subterms of the current sequent, both relying on the same special syntax to
+identify a term occurrence.
+
+The first way is to use this special syntax to tell the
+tactic what occurrences of a wanted term should be affected.
+The second is to prepare the sequent with another tactic called
+\TAC{pattern} and then apply the real tactic. Note that the choice is not
+left to the user, since some tactics needs the sequent to be prepared
+with pattern and do not accept directly this special syntax.
+
+The idea is that to identify a subterm of the sequent we can
+write it and say that we want, for example, its third and fifth
+occurrences (counting from left to right). In our previous example,
+to change only the left part of the equivalence, the correct command
+would be:
+\begin{grafite}
+ change n at 2 in H with (O + n)
+\end{grafite}
+meaning that in the hypothesis \texttt{H} the \texttt{n} we want to change is
+the second we encounter proceeding from left to right.
+
+The tactic \TAC{pattern} computes a
+$\beta$-expansion of a part of the sequent with respect to some
+occurrences of the given term. In the previous example the following
+command:
+\begin{grafite}
+ pattern n at 2 in H
+\end{grafite}
+would have resulted in the sequent:
+\sequent{n: nat\\m : nat\\H: (fun~n0: nat => m + n = n0)~n}{m = 0}
+where \texttt{H} is $\beta$-expanded over the second \texttt{n}
+occurrence.
+
+At this point, since \COQ{} unification algorithm is essentially first-order,
+the application of an elimination principle (a term of type\linebreak
+$\forall P.\forall
+x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with
+\texttt{(fun n0: nat => m + n = n0)}.
+
+Since \TAC{rewrite}, \TAC{replace} and several other tactics boil down to
+the application of the equality elimination principle, the previous
+trick implements the expected behavior.
+
+The idea behind this way of identifying subterms in not really far
+from the idea behind patterns, but fails in extending to
+complex notation, since it relies on a mono-dimensional sequent representation.
+Real mathematical notation places arguments upside-down (like in indexed sums or
+integrations) or even puts them inside a bidimensional matrix.
+In these cases using the mouse to select the wanted term is probably the
+more effective way to tell the system what to do.
+One of the goals of \MATITA{} is to use modern publishing techniques,
+so we prefer our method that does not discourage the use of complex layout schemata.
+
+In \MATITA{}, tactics accepting pattern arguments can be more expressive than
+the equivalent tactics in \COQ{} since variables bound in the pattern context,
+can occur in context-dependent arguments. For example, consider the sequent:
+\sequent{n: nat\\x: nat\\H: \forall m. n + m*n = x + m}{m = O}
+In \MATITA{} the user can issue the command:
+\begin{grafite}
+change in H: \forall _. (? ? % ?) with (S m) * n.
+\end{grafite}
+to change $n+m*n$ with $(S~m)*n$. To achieve the same effect in \COQ, the
+user is forced to change the whole hypothesis rewriting its right hand side
+as well.
+
+\subsection{Tacticals}
+\label{sec:tinycals}
+
+The procedural proof language implemented in \MATITA{} is pretty standard,
+with a notable exception for tacticals.
+
+Tacticals first appeared in LCF~\cite{lcf} as higher order tactics.
+They can be seen as control flow constructs like looping, branching,
+error recovery and sequential composition.
+
+The following simple example shows a \COQ{} script made of four dot-terminated
+commands:
+\begin{grafite}
+Theorem trivial:
+ forall A B:Prop,
+ A = B -> ((A -> B) /\ (B -> A)).
+ intros [A B H].
+ split; intro;
+ [ rewrite < H; assumption
+ | rewrite > H; assumption
+ ].
+Qed.
+\end{grafite}
+
+The third command is an application of the sequencing tactical \OP{$\ldots$~;~$\ldots$},
+that combines the tactic \TAC{split} with the application of the branching
+tactical \OP{$\ldots$~;[~$\ldots$~|~$\ldots$~|~$\ldots$~]} to other tactics or tacticals.
+
+The usual implementation of tacticals executes them atomically as any
+other command. In \MATITA{} this is not the case: each punctuation
+symbol is executed as a single command.
+
+\subsubsection{Common issues of tacticals}
+We will examine the two main problems of procedural proof languages:
+maintainability and readability.
+
+Tacticals are not only used to make scripts shorter by factoring out
+common cases and repeating commands. They are the primary way of making
+scripts more maintainable. They also have the well-known duty of
+structuring the proof using the branching tactical.
+
+However, authoring a proof structured with tacticals is annoying.
+Consider for example a proof by induction, and imagine you
+are using one of the state of the art graphical interfaces for proof assistant
+like Proof General. After applying the induction principle you have to choose:
+immediately structure the proof or postpone the structuring.
+If you decide for the former you have to apply the branching tactical and write
+at once tactics for all the cases. Since the user does not even know the
+generated goals yet, he can only replace all the cases with the identity
+tactic and execute the command, just to receive feedback on the first
+goal. Then he has to go one step back to replace the first identity
+tactic with the wanted one and repeat the process until all the
+branches are closed.
+
+One could imagine that a structured script is simpler to understand.
+This is not the case.
+A proof script, being not declarative, is not meant to be read.
+However, the user has the need of explaining it to others.
+This is achieved by interactively re-playing the script to show each
+intermediate proof status. Tacticals make this operation uncomfortable.
+Indeed, a tactical is executed atomically, while it is obvious that it
+performs lot of smaller steps we are interested in.
+To show the intermediate steps, the proof must be de-structured on the
+fly, for example replacing \OP{;} with \OP{.} where possible.
+
+\MATITA{} has a peculiar tacticals implementation that provides the
+same benefits as classical tacticals, while not burdening the user
+during proof authoring and re-playing.
+
+\subsubsection{The \MATITA{} approach}
+
+\begin{table}
+ \caption{Concrete syntax of tacticals\strut}
+ \label{tab:tacsyn}
+\hrule
+\[
+\begin{array}{@{}rcll@{}}
+ \NT{punctuation} &
+ ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
+ \NT{block\_kind} &
+ ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
+ \NT{block\_delim} &
+ ::= & \verb+begin+ ~|~ \verb+end+ & \\
+ \NT{command} &
+ ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delim} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} \\
+\end{array}
+\]