From 63d1734e6da8a8e2fc70a8e8476ef6b7ae5344c4 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 31 Jan 2006 12:19:16 +0000 Subject: [PATCH] /me reviewed automation subsection --- helm/papers/matita/matita2.tex | 77 ++++++++++++++++++---------------- 1 file changed, 40 insertions(+), 37 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 516eacbde..f9f5565c2 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -60,6 +60,7 @@ \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}} @@ -1174,28 +1175,30 @@ 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 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 @@ -1204,51 +1207,51 @@ 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 +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} -- 2.39.2