brokers.
In Sect. \ref{architecture} we present the architecture of \hbugs{}.
+ An usage session is shown in Sect. \ref{usage}.
Further implementation details are given in Sect. \ref{implementation}.
Sect. \ref{tutors} is an overview of the tutors that have been implemented.
As usual, the final section of this paper is devoted to conclusions and future works.
\hbugs{} tutors act as MONET services.
\section{An \hbugs{} Session Example}
+\label{usage}
In this section we describe a typical \hbugs{} session. The aim of the
session is to solve the following easy exercise:
\begin{exercise}
-Let $x$ be a generic real numbers. Using the \helm{} proof-engine,
+Let $x$ be a generic real number. Using the \helm{} proof-engine,
prove that
\begin{displaymath}
x = \frac{(x+1)*(x+1) - 1 - x*x}{2}
\end{displaymath}
\end{exercise}
-\myincludegraphics{step1}{t}{12cm}{Example session.}
- {Example session.}
-%\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
-% {Example session, snapshot 2.}
-
-Let us suppose that the \hbugs{} broker is already running and that several
+Let us suppose that the \hbugs{} broker is already running and that the
tutors already registered themselves to the broker.
When the user starts \texttt{gTopLevel}, the system registers itself to
the broker, that sends back the list of available tutors. By default,
-\texttt{gTopLevel} notifies the broker its intention of subscribing to every
+\texttt{gTopLevel} notifies to the broker its intention of subscribing to every
tutor available. The user can always open a configuration window where she
is presented the list of available tutors and she can independently subscribe
-and unsubscribe each tutor.
+and unsubscribe the system to each tutor.
+
+\myincludegraphics{step1}{t}{12cm}{Example session.}
+ {Example session.}
+%\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
+% {Example session, snapshot 2.}
The user can now insert into the system the statement of the theorem and start
proving it. Let us suppose that the first step of the user is proving
that the denominator 2 is different from 0. Once that this technical result
-is proven, the user must prove the goal shown in the upper left corner
+is proven, the user must prove the goal shown in the upper right corner
of the window in background in Fig. \ref{step1}.
While the user is wondering how to proceed in the proof, the tutors are
the proof by exchanging the two sides of the equality.
The second hint suggests to reduce both sides of the equality to their normal
form by using only reductions which are justified by the ring structure of the
-real numbers. The two normal forms, though, are so different that the proof is
+real numbers; the two normal forms, though, are so different that the proof is
not really simplified.
All the residual 21 hints suggest to apply one lemma from the distributed
-library of \helm{}.
+library of \helm{}. The user can look at the statement of the lemma by clicking
+on its URI.
-The user can look at the list of suggestions and realize that a good one is
-that of applying the lemma \texttt{r\_Rmult\_mult} which
-allow\footnote{The user can always look at
-the statement of a theorem by clicking on its URI.} to multiply both equality
+The user can now look at the list of suggestions and realize that a good one is
+applying the lemma \texttt{r\_Rmult\_mult} that allows to multiply both equality
members by the same scalar\footnote{Even if she does not receive the hint, the
user probably already knows that this is the right way to proceed. The
difficult part where the hint helps is guessing what is the name of the lemma
the lemma, reducing the proof to closing three new goals. The first one asks
the user the scalar to use as an argument of the previous lemma; the second
one states that the scalar is different from 0; the third lemma (the main
-one) asks to prove the equality between the products of the two old members
-with the scalar.
+one) asks to prove the equality between the two new members.
% is shown in Fig. \ref{step2} where $?_3[H;x]$ stands for
% the still unkown scalar argument, which can have only $H$ and $x$ as
% free variables.
The user proceeds by istantiating the scalar with the number 2. The
-\texttt{Assumption} tutor now suggests to close the second goal by applying
-the hypothesis $H$. No useful suggestions, instead, are generated for the
-main goal $2x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$.
-To proceed in the proof, indeed, the user needs to symplify the
+\texttt{Assumption} tutor now suggests to close the second goal (that
+states that $2 \neq 0$) by applying the hypothesis $H$.
+No useful suggestions, instead, are generated for the main goal
+$2*x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$.
+To proceed in the proof the user needs to symplify the
expression using the lemma $Rinv\_r\_simpl\_m$ that states that
$\forall x,y.\;y = x * y * x^{-1}$. Since we do not provide yet any tutor
suggesting symplifications, the user must find out this symplication by
himself. Once she founds it, the goal is reduced to proving that
-$2x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the
+$2*x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the
\texttt{Ring} tutor, that suggests\footnote{The \texttt{Ring} suggestion is
just one of the 22 hints that the user receives. It is the only hint that
-does not open new goals.} to the user how to directly finish the proof.
+does not open new goals, but the user right now does not have any way to know
+that.} to the user how to directly finish the proof.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Comandi da dare a gTopLevel %
projects / helm.git / commitdiff