\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}.
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}
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.
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.
the proof found: the client applies the hint reconstructing (and checking
the correctness of) the proof from the witness, without having to
re-discover the proof itself.
+ \ednote{Zack: che ne dici di un "reinvent the whell" qui sopra? fa sempre
+ effetto ...}
An alternative implementation where the tutors are trusted would simply
send back to the client a new proof-status. Upon receiving the
\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. Like clients\ednote{Zack: mi
+ pare che questo sia un caso in cui si debba usare "as" e non like, ma non ne
+ sono certo}, 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
+ 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.}
of $n \le n$ is simply the application of the first constructor to
$n$ and a proof of $n \le m$ is the application of the second
constructor to $n,m$ and a proof of $n \le m$.}.
+ \ednote{Zack: non e' necessario specificare che stai parlando di numeri
+ naturali nella footnote?}
Since disjunction, conjunction, existential quantification and
Leibniz equality are particular cases of inductive propositions,
all the other tutors of this class are instantiations of the
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 / commitdiff