\end{figure}
}
-\usepackage[show]{ed}
-\usepackage{draftstamp}
+%\usepackage[show]{ed}
+%\usepackage{draftstamp}
\newcommand{\musing}{\texttt{musing}}
\newcommand{\musings}{\texttt{musings}}
\begin{abstract}
We present a planning broker and several Web-Services for automatic deduction.
- Each Web-Service implements one of the tactics usually available in an
- interactive proof-assistant. When the broker is submitted a "proof status" (an
- unfinished proof tree and a focus on an open goal) it dispatches the proof to
+ Each Web-Service implements one of the tactics usually available in
+ interactive proof-assistants. When the broker is submitted a "proof status" (an
+ incomplete proof tree and a focus on an open goal) it dispatches the proof to
the Web-Services, collects the successful results, and send them back to the
client as "hints" as soon as they are available.
The big challenge for the next future is to provide stable and reliable
services over this disorganized, unreliable and ever-evolving architecture.
- The standard solution is providing a further level of
- stable services (called \emph{brokers}) that behave as common gateway/address
+ The standard solution is to provide a further level of
+ stable services (called \emph{brokers}) that behave as common gateways/addresses
for client applications to access a wide variety of services and abstract over
them.
Computer Algebra Systems; the second ones provide interfaces to well-known
theorem provers.
Proof-planners, proof-assistants, CAS and
- domain-specific problem solvers are natural candidates to be client of these
+ domain-specific problem solvers are natural candidates to be clients of these
services. Nevertheless, so far the number of examples in the literature has
been extremely low and the concrete benefits are still to be assessed.
each tutor try to make progress in the proof and, in case
of success, notify the client that shows an \emph{hint} to the user.
The broker is an instance of the homonymous entity of the MONET framework.
- The tutors are MONET services. Another \ws (which is not described in this
+ The tutors are MONET services. Another \ws{} (which is not described in this
paper and which is called Getter \cite{zack}) is used to locate and download
mathematical entities; the Getter plays the role of the Mathematical Object
Manager in the MONET framework.
In Sect. \ref{architecture} we present the architecture of \hbugs{}.
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 paper ends with the conclusions and future works.
+ As usual, the final section of this paper is devoted to conclusions and future works.
\section{An \hbugs{} Bird's Eye View}
\label{architecture}
Each actor present one or more \ws{} interfaces to its neighbors \hbugs{}
actors.
- In this section we will detail the role and requirements of each kind of
+ In this section we detail the role and requirements of each kind of
actors and discuss about the correspondences between them and the MONET
entities described in \cite{MONET-Overview}.
new status are sent to the broker as soon as the proof change (e.g. when the
user applies a tactic or when a new proof is started) and hints are shown to
the user be the means of some effect in the user interface (e.g. popping a
- dialog box or enlightening a tactic button).\ednote{CSC: questo \'e un
- possibile posto dove mettere una reference a una mini-sessione interattiva.
- \'E l'appendice un posto dove metterla?}
-
- \myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces}
- {\hbugs{} \wss{} interfaces}
+ dialog box or enlightening a tactic button).
\hbugs{} clients act as MONET clients and ask brokers to provide access to a
set of services (the tutors). \hbugs{} has no actors corresponding to
mathematical items in the \helm{} library.
The proof status that are exchanged
by the \hbugs{} actors, instead, are built on the fly and are neither
- stored nor are given an unique identifier (URI) to be managed by the
+ stored nor given an unique identifier (URI) to be managed by the
Getter.
\paragraph{Brokers}
+ \myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces}
+ {\hbugs{} \wss{} interfaces}
+
Brokers are the key actors of the \hbugs{} architecture since they
act as intermediaries between clients and tutors. They behave as \wss{}
providers and requesters for \emph{both} clients and tutors, see Fig.
etc.). The only requirement is that there exists an agreement on the
formats of proof status and hints.
- Tutors act both as \ws{} providers and requesters for the broker. As
+ Tutors act both as \ws{} providers and requesters for the broker, see Fig.
+ \ref{interfaces}. As
providers, they wait for commands requesting to start a new \musing{} on
a given proof status or to stop an old, out of date, \musing{}. As
requesters, they signal to the broker the end of a \musing{} along with its
- outcome (an hint in case of success or a notification of failure).
+ outcome (an hint in case of success or a failure notification).
\hbugs{} tutors act as MONET services.
\section{An \hbugs{} Session Example}
+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,
+prove that
+\begin{displaymath}
+x = \frac{(x+1)*(x+1) - 1 - x*x}{2}
+\end{displaymath}
+\end{exercise}
+
+\myincludegraphics{step1}{t}{12cm}{Example session, snapshot 1.}
+ {Example session, snapshot 1.}
+%\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
+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
+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.
+
+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
+of the window in background in Fig. \ref{step1}.
+
+While the user is wondering how to proceed in the proof, the tutors are
+trying to progress in the proof. After a while, the tutors' suggestions
+start to appear in the lower part of the \hbugs{} interface window
+(the topmost window in Fig. \ref{prima}). In this case, the tutors are able
+to produce 23 hints. The first and not very useful hint suggests to proceed in
+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
+not really simplified.
+All the residual 21 hints suggest to apply one lemma from the distributed
+library of \helm{}.
+
+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
+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
+to apply.}.
+Double-clicking on the hint automatically applies
+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.
+% 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*\frac{((x+1)*(x+1)-1-x*x)}{2}$.
+To proceed in the proof, indeed, 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
+\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.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Comandi da dare a gTopLevel %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% New proof:
+% !x.(not (eqT ? (Rplus R1 R1) R0)) -> (eqT ? x (Rdiv (Rminus (Rminus (Rmult (Rplus x R1) (Rplus x R1)) R1) (Rmult x x)) (Rplus R1 R1)))
+% Intros x H
+% Apply r_Rmult_mult
+% 3: Apply H
+% Simpl (per fare unfold di Rdiv)
+% Rewrite <-
+% (Rmult_assoc (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) (Rinv (Rplus R1 R1)))
+% Rewrite ->
+% (Rinv_r_simpl_m (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) H)
+% *** Ring
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Implementation's Highlights}
\label{implementation}
exchange status in WSDL using the XML Schema type system, we have chosen an
XML format as the target format for the serialization.
- A schematic representation of the gTopLevel internal status is depicted in
- Fig. \ref{status}. Each proof is represented by a tuple of four elements:
+% A schematic representation of the gTopLevel internal status is depicted in
+% Fig. \ref{status}.
+ Each proof is represented by a tuple of four elements:
\emph{uri}, \emph{metasenv}, \emph{proof}, \emph{thesis}.
- \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
- status}
+% \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
+% status}
\begin{description}
\item[uri]: an URI chosen by the user at the beginning of the proof
In order to complete the proof, the user has to instantiate every
metavariable in the proof with a proof of the corresponding goal.
Each goal is identified by an unique identifier and has a context
- and a type ( the goal thesis). The context is a list of named
+ and a type (the goal thesis). The context is a list of named
hypotheses (declarations and definitions). Thus the context and the goal
thesis form a sequent, which is the statement of the proof that will
be used to instantiate the metavariable occurrences.
\ws{}.
Additionally tutors are required to send an human readable description of
their capabilities; this information could be used by client's user to
- decide which tutors he needs to subscribe to. Like clients, tutors can
+ decide which tutors he needs to subscribe to. As the clients, tutors can
unregister from brokers using \texttt{Unregister\_broker} method.
- Each time the client status change, the status is sent to the
+ Each time the client status change, it get sent sent to the
broker using its \texttt{Status} method. Using both clients registry (to
lookup client's subscription) and tutors registry (to check if some tutors
has unsubscribed), the broker is able to decide to which tutors the
- new status must be forwarded.\ednote{CSC: qui o nei lavori futuri parlare
- della possibilit\'a di avere un vero brocker che multiplexi le richieste
- dei client localizzando i servizi, etc.}
+ new status have to be forwarded.
+% \ednote{CSC: qui o nei lavori futuri parlare
+% della possibilit\'a di avere un vero brocker che multiplexi le richieste
+% dei client localizzando i servizi, etc.}
The forwarding operation is performed using the \texttt{Start\_musing}
method of the tutors, that is a request to start a new computation
to share the cache of loaded (and type-checked) theorems.
As we will explain in Sect. \ref{tutors}, this feature turns out to be
really useful for tactics that rely on a huge but fixed set of lemmas,
- as every reflexivite tactic.
+ as every reflexive tactic.
The implementation of a tutor with the described architecture is not that
difficult having a language with good threading capabilities (as OCaml has)
or more constructors when the goal thesis is an inductive type or a
proposition inductively defined according to the declarative
style\footnote{An example of a proposition that can be given in
- declarative style is the $\le$ relation: $\le$ is the smallest relation
+ declarative style is the $\le$ relation over natural numbers:
+ $\le$ is the smallest relation
such that $n \le n$ for every $n$ and $n \le m$ for every $n,m$ such
that $n \le p$ where $p$ is the predecessor of $m$. Thus, a proof
of $n \le n$ is simply the application of the first constructor to
To test the productivity impact of intelligent tutors, we have implemented
a tutor that is interfaced with the \helm{}
- Search-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that
+ Search-Engine\footnote{\url{http://helm.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
To conclude, \hbugs{} is a nice experiment meant to understand whether the
current \wss{} technology is mature enough to have a concrete and useful
- impact on the daily work of users of proof-assistants. So far, only the tutor
+ impact on the daily work of proof-assistants users. So far, only the tutor
that is interfaced with the \helm{} Search-Engine has effectively increased
the productivity of experts users. The usefulness of the tutors developed for
beginners, instead, need further assessment.
Deduction Systems via the Logic Broker Architecture. In Proceedings
of the Eighth Calculemus symphosium, St. Andrews, Scotland, 6--7 August 2000.
-\bibitem{ws3} O. Caprotti. Symbolic Evaluator Service. Project Report of
+\bibitem{ws2} O. Caprotti. Symbolic Evaluator Service. Project Report of
the MathBrocker Project, RISC-Linz, Johannes Kepler University, Linz,
Austria, May 2002.
\bibitem{zack} S. Zacchiroli. \emph{Web services per il supporto alla
dimostrazione interattiva}, Master Thesis, University of Bologna, 2002.
-\bibitem{ws4} J. Zimmer and L. Dennis. Inductive Theorem Proving and
+\bibitem{ws3} J. Zimmer and L. Dennis. Inductive Theorem Proving and
Computer Algebra in the MathWeb Software Bus. In Proceedings of the 10th
CALCULEMUS Symposium 2002, 3--5 July 2002.
-\bibitem{ws2} R. Zippel. The MathBus. In Workshop on Internet Accessible
+\bibitem{ws4} R. Zippel. The MathBus. In Workshop on Internet Accessible
Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999.
\end{thebibliography}
projects / helm.git / blobdiff