+\subsection{Tacticals}
+\ASSIGNEDTO{gares}\\
+There are mainly two kinds of languages used by proof assistants to recorder
+proofs: tactic based and declarative. We will not investigate the philosophy
+aroud the choice that many proof assistant made, \MATITA{} included, and we will not compare the two diffrent approaches. We will describe the common issues of the first one and how \MATITA{} tries to solve them.
+
+First we must highlight the fact that proof scripts made using tactis are
+particularly unreadable. This is not a big deal for the user while he is
+constructing the proof, but is considerably a problem when he tries to reread
+what he did or when he shows his work to someone else.
+
+Another common issue for tactic based proof scripts is their mantenibility.
+Huge libraries have been developed, and backward compatibility is a really time
+consuming task. This problem is usually ameliorated with tacticals, that
+help in structuring proofs and consequently their maintenance, but have a bad
+counterpart in script readability. Since tacticals are executed atomically,
+the common practice of executing again a script to review all the proof steps
+doesn't work at all. This issue in addition to the really poor feeling that a
+list of tactics gives about the proof makes script rereading particularly hard.
+
+\MATITA{} uses a language of tactics and tacticals, but adopts a peculiar
+strategy to make this technique more user friendly without loosing in
+mantenibility or expressivity.
+
+\subsubsection{Tacticals overview}
+Before describing the peculiarities of \MATITA{} tacticals we briefly introduce what tacticals are and where they can be useful.
+
+Tacticals first appered in LCF(cita qualcosa) and can be seen as programming
+constructs, like looping, branching, error recovery or sequential composition.
+For example $tac_1~.~tac_2$ executes the first tactic and applies the second
+only to the first goal opened by $tac_1$. Baranching can be used to specify a
+diffrent tactic to apply to each new goal opened by another tactic, for example
+$tac_1\verb+;[+~tac_{1.1}~\verb+|+~tac_{1.2}~\verb+|+~\cdots~|~tac_{1.n}~\verb+]+$
+applies respectively $tac_{1.i}$ to the $i$-th goal opened by $tac_1$. Looping
+can be used to iterate a tactic until it works: $\verb+repeat+~tac$ applies
+$tac$ to the current goal, and again $tac$ to the eventually resulting goals
+until all goal are closed or the tactic fails.
+
+\begin{table}
+ \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
+\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\_delimiter} &
+ ::= & \verb+begin+ ~|~ \verb+end+ & \\
+ \NT{tactical} &
+ ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
+While one whould expect to find structured constructs like
+$\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
+This is essential for base idea behind matita tacticals: step-by-step execution.
+
+\subsubsection{\MATITA{} Tinycals}
+The low-level tacticals implementation of \MATITA{} allows a step-by-step execution of a tactical, that substantially means that a $\NT{block\_kind}$ is not executed as an atomic operation. This has two major benefits for the user, even being a so simple idea:
+\begin{description}
+\item[Proof structuring]
+ is much easyer. Consider for example a proof by induction, and imagine you are using classical tacticals. After applying the
+ induction principle, with one step tacticals, you have to choose: structure
+ the proof or not. If you decide for the former you have to branch with
+ \verb+[+ and write tactics for all the cases separated by \verb+|+ and the
+ close the tactical with
+ \verb+]+. You can replace most of the cases by the identity tactic just to
+ concentrate only on the first goal, but you will have to go one step back and
+ one further every time you add something inside the tactical. And if you are
+ boared of doing so, you will finish in giving up structuring the proof and
+ write a plain list of tactics.\\
+ With step-by-step tacticals you can apply the induction principle, and just
+ open the branching tactical \verb+[+. Then you can interact with the system
+ reaching a proof of the first case, without having to specify the whole
+ branching tactical. When you have proved all the induction cases, you close
+ the branching tactical with \verb+]+ and you are done with a structured proof.
+\item[Rereading]
+ is possible. Going on step by step shows exactly what is going on.
+ Consider again a proof by induction, that starts applying the induction
+ principle and suddenly baranches with a \verb+[+. This clearly separates all
+ the induction cases, but if the square brackets content is executed in one
+ single step you completely loose the possibility of rereading it. Again,
+ executing step-by-step is the way you whould like to review the
+ demonstration. Remember tha understandig the proof from the script is not
+ easy, and only the execution of tactics (and the resulting transformed goal)
+ gives you the feeling of what is goning on.
+\end{description}
+
+