\newcommand{\URI}[1]{\texttt{#1}}
\newcommand{\OP}[1]{``\texttt{#1}''}
\newcommand{\FILE}[1]{\texttt{#1}}
+\newcommand{\TAC}[1]{\texttt{#1}}
\newcommand{\NOTE}[1]{\ednote{#1}{}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
\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 the long run, one would expect to work with a proof assistant
+like \MATITA, using only 3 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.
+this is one of the main development direction of \MATITA.
-Even in this field, the underlying phisolophy of Matita is to
+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
+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
+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 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.
+The basic tactic merely iterates the use of the \TAC{apply} tactic
+(with no \TAC{intro}). The search tree may be pruned according to 2
+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
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
+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 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 {\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
+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 weigthing functions
comprising Knuth-Bendix ordering (kbo) and recursive path ordering (rpo),
-that integrates particualry well with normalization.
+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 {\em demodulate}
-tactic, which can be seen as a kind of generalization of {\em simplify}.
+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{verbatim}
+\begin{grafite}
theorem example1:
- \forall x:nat. (x+1)*(x-1)=x*x - 1.
+ \forall x: nat. (x+1)*(x-1) = x*x - 1.
intro.
apply (nat_case x)
-[simplify;reflexivity
-|intro;demodulate;reflexivity]
+[ 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.
+ \forall x, y: nat. (x+y)*(x+y) = x*x + 2*x*y + y*y.
+intros; demodulate; reflexivity;
qed.
-\end{verbatim}
+\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}
projects / helm.git / commitdiff