From ed308fc03be5397081ac0e00bbc73b3f71da1e67 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 31 Jan 2006 10:13:20 +0000
Subject: [PATCH] Added a new section on automation

---
 helm/papers/matita/matita.bib  |  9 +++++
 helm/papers/matita/matita2.tex | 74 +++++++++++++++++++++++++++++++++-
 2 files changed, 82 insertions(+), 1 deletion(-)

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index 8aa1c4882..7d98905d5 100644
--- a/helm/papers/matita/matita.bib
+++ b/helm/papers/matita/matita.bib
@@ -1,3 +1,12 @@
+@inproceedings{paramodulation,
+  author = "Robert Nieuwenhuis and Alberto Rubio",
+  title = "Paramodulation-based thorem proving",
+  booktitle = "Handbook of Automated Reasoning",
+  editor = "John Alan Robinson and Andrei Voronkov",
+  pages = "471--443",
+  publisher = "Elsevier and MIT Press",
+  year = 2001,
+}
 
 @inproceedings{latexmathml,
  author = {Luca Padovani},
diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 2332ced9d..65b5882af 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1171,8 +1171,80 @@ 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: 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}
-- 
2.39.2