+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.