\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: Intro, Elim, and Auto
+(possibly integrated by a moderate use of 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 phisolophy 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 Auto tactic;
+in Matita, it is the system itself that authomatically 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 performs an iterated use of the Apply tactic
+(with no Intro). The research tree may be pruned according to two
+main parameters: the {\em depth} (whit the obvious meaning), and the
+{\em 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 Auto tactic
+should be compared with Coq's EAuto.
+
+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 theorem
+provers.
+
+The given-clause algorithm is essentially composed by an alternation
+of a {\em saturation} phase, deriving new facts by a set of active
+facts and a new {\em given} clause suitably selected from a set of passive
+equations,
+and a {\em demodulation} phase that tries to simplify the equations
+orienting them according to a suitable weight associated with terms.
+Matita currently supports several different weigthing functions
+comprising Knuth-Bendix ordering (kbo) and recursive path ordering (rpo),
+that integrates particualry well with normalization.
+
+Demodulation alone is already a quite powerful technique, and
+it has been turned into a tactic by itself: the {\em demodulate}
+tactic, which can be seen as a kind of generalization of {\em simplify}.
+The following portion of script describes two
+interesting cases of application of this tactic (both of them relying
+on elementary arithmetic equations):
+
+\begin{verbatim}
+theorem example1:
+ \forall x:nat. (x+1)*(x-1)=x*x - 1.
+intro.
+apply (nat_case x)
+[simplify;reflexivity
+|intro;demodulate;reflexivity]
+qed.
+
+theorem example2:
+ \forall x,y:nat. (x+y)*(x+y) = x*x + 2*x*y + y*y.
+intros;demodulate;reflexivity.
+qed.
+\end{verbatim}
+
+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.
+
-\TODO{sezione sull'automazione}
\subsection{Naming convention}
\label{sec:naming}
projects / helm.git / commitdiff