\section{???}
\label{implementation}
-\section{???}
+\section{The \hbugs Tutors}
\label{tutors}
+To test the \hbugs architecture and to assess the utility of a suggestion
+engine for the end user, we have implemented several tutors. In particular,
+we have investigated three classes of tutors:
+\begin{enumerate}
+ \item \emph{Tutors for beginners}. These are tutors that implement tactics
+ which are neither computationally expensive nor difficult to understand:
+ an expert user can always understand if the tactic can be applied or not
+ withouth having to try it. For example, the following implemented tutors
+ belong to this class:
+ \begin{itemize}
+ \item \emph{Assumption Tutor}: it ends the proof if the thesis is
+ equivalent\footnote{The equivalence relation is convertibility. In some
+ cases, expecially when non-trivial computations are involved, the user
+ is totally unable to figure out the convertibility of two terms.
+ In these cases the tutor becomes handy also for expert users.}
+ to one of the hypotheses.
+ \item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad
+ adsurdum} if one hypothesis is equivalent to $False$.
+ \item \emph{Symmetry Tutor}: if the goal thesis is an equality, it
+ suggests to apply the commutative property.
+ \item \emph{Left/Right/Exists/Split/Constructor Tutors}: the Constructor
+ Tutor suggests to proceed in the proof by applying one or more
+ constructors when the goal thesis is an inductive type or a
+ proposition inductively defined according to the declarative style.
+ Since disjunction, conjunction and existential quantifications are
+ particular cases of inductive propositions,
+ all the other tutors of this class implements restrictions of the
+ the Constructor tactic: Left and Right suggest to prove a disjunction
+ by proving its left/right member; Split reduces the proof of a
+ conjunction to the two proof of its members; Exists suggests to
+ prove an existential quantification by providing a
+ witness\footnote{This task is left to the user.}.
+ \end{itemize}
+ Beginners, when first faced with a tactic-based proof-assistant, get
+ lost quite soon since the set of tactics is large and their names and
+ semantics must be remembered by heart. Tutorials are provided to guide
+ the user step-by-step in a few proofs, suggesting the tactics that must
+ be used. We believe that our beginners tutors can provide an auxiliary
+ learning tool: after the tutorial, the user is not suddendly left alone
+ with the system, but she can experiment with variations of the proof given
+ in the tutorial as much as she like, still getting useful suggestions.
+ Thus the user is allowed to focus on learning how to do a formal proof
+ instead of wasting efforts trying to remember the interface to the system.
+ \item{Tutors for Computationally Expensive Tactics}. Several tactics have
+ an unpredictable behaviour, in the sense that it is unfeasible to understand
+ wether they will succeed or they will failt when applied and what will be
+ their result. Among them, there are several tactics either computationally
+ expensive or resources consuming. In the first case, the user is not
+ willing to try a tactic and wait for a long time just to understand its
+ outcome: she would prefer to keep on concentrating on the proof and
+ have the tactic applied in background and receive out-of-band notification
+ of its success. The second case is similar, but the tactic application must
+ be performed on a remote machine to avoid overloading the user host
+ with several concurrent resource consuming applications.
+
+ Finally, several complex tactics and in particular all the tactics based
+ on reflexive techniques depend on a pretty large set of definitions, lemmas
+ and theorems. When these tactics are applied, the system needs to retrieve
+ and load all the lemmas. Pre-loading all the material needed by every
+ tactic can quickly lead to long initialization times and to large memory
+ footstamps. A specialized tutor running on a remote machine, instead,
+ can easily pre-load the required theorems.
+
+ As an example of computationally expensive task, we have implemented
+ a tutor for the \emph{Ring} tactic. The tutor is able to prove an equality
+ over a ring by reducing both members to a common normal form. The reduction,
+ which may require some time in complex cases,
+ is based on the usual commutative, associative and neutral element properties
+ of a ring. The tactic is implemented using a reflexive technique, which
+ means that the reduction trace is not stored in the proof-object itself:
+ the type-checker is able to perform the reduction on-the-fly thanks to
+ the conversion rules of the system. As a consequence, in the library there
+ must be stored both the algorithm used for the reduction and the proof of
+ correctness of the algorithm, based on the ring axioms. This big proof
+ and all of its lemmas must be retrieved and loaded in order to apply the
+ tactic. The Ring tutor loads and cache all the required theorems the
+ first time it is conctacted.
+ \item{Intelligent Tutors}. Expert users can already benefit from the previous
+ class of tutors. Nevertheless, to achieve a significative production gain,
+ they need more intelligent tutors implementing domain-specific theorem
+ provers or able to perform complex computations. These tutors are not just
+ plain implementations of tactics or decision procedures, but can be
+ more complex software agents interacting with third-parties software,
+ such as proof-planners, CAS or theorem-provers.
+
+ To test the productivity impact of intelligent tutors, we have implemented
+ a tutor that is interfaced with the HELM
+ Proof-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that
+ is able to look for every theorem in the distributed library that can
+ be applied to proceed in the proof. Even if the tutor deductive power
+ is extremely limited\footnote{We do not attempt to check if the new goals
+ obtained applying a lemma can be authomatically proved or, even better,
+ auhomatically disproved to reject the lemma.}, it is not unusual for
+ the tutor to come up with precious hints that can save several minutes of
+ works that would be spent in proving again already proven results or
+ figuring out where the lemmas could have been stored in the library.
+\end{enumerate}
+
+Once the code that implements a tactic or decision procedure is available,
+transforming it into a tutor is not a difficult task, but it is surely
+repetitive and error prone.
\section{???}
\label{conclusions}
projects / helm.git / commitdiff