capabilities \cite{ws1,ws2,ws3,ws4}: the first ones are implemented on top of
Computer Algebra Systems; the second ones provide interfaces to well-known
theorem provers.
- Proof-planners, proof-assistants, CAS and
+ Proof-planners, proof-assistants, CASs and
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 insufficient to fully assess the concrete benefits of the framework.
it is then ``shared'' by the client and all the tutors until the client
submits the next problem. For instance, replacing the client with a CAS and
all the tutors with agents implementing different resolution methods for
- differential equations would not require any change in the broker. Notice,
- however, that all the tutors must expose the same interface to the broker.
+ differential equations would not require any change in the broker. Notice
+ that all the tutors must expose the same interface to the broker.
The MONET architecture specification does not state explicitly whether the
service and broker answers can be asynchronous. Nevertheless, the
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
+When the user starts our proof-engine \texttt{gTopLevel}, the system registers itself to
the broker, that sends back the list of available tutors. By default,
\texttt{gTopLevel} notifies to the broker its intention of subscribing to every
tutor available. The user can always open a configuration window where she
In our implementation the client does not trust the tutors hints:
being encoded as references to available tactics imply
- that an \hbugs{} client, upon receival of a hint, simply try to replay
+ that an \hbugs{} client, at the receipt of a hint, simply try to replay
the work
done by a tutor on the local copy of the proof. The application of the hint
can even fail to type check and the client copy of the proof can be left
using its \texttt{Musing\_completed} method; the broker can now remove the
\musing{} entry from the \musings{} registry and, depending on its outcome,
inform the client. In case of success one of the \texttt{Musing\_completed}
- arguments is a hint to be sent to the client, otherwise there is no need to
+ arguments is a hint to be sent to the client; otherwise there is no need to
inform him and the \texttt{Musing\_completed} method is called
just to update the \musings{} registry.
to apply or ignore them. A broker is provided to decouple the clients and
the tutors and to allow the client to locate and invoke the available remote
services. The whole architecture is an instance of the MONET architecture
- for Mathematical \wss{}.
+ for Mathematical \wss{}. It constitutes a reimplementation of the core
+ features of the pioneering \OmegaAnts{} system in the new \wss{}
+ framework.
A running prototype has been implemented as part of the
\helm{} project \cite{helm}
Those negative suggestions could be reflected in the user interface by
deactivating commands to narrow the choice of tactics available to the user.
This approach could be interesting especially for novice users, but requires
- the client to trust other actors a bit more than in the current approach.
+ the client to increase their level of trust in the other actors.
We plan also to add some rating mechanism to the architecture. A first
improvement in this direction could be distinguishing between hints that, when
could be a measure that try to minimize the size of the generated proof,
privileging therefore non-overkilling solutions \cite{ring}.
- We are also considering to follow the \OmegaAnts{} path more closely adding
+ We are also considering to follow the \OmegaAnts{} path adding
``recursion'' to the system so that the proof status resulting from the
application of old hints are cached somewhere and could be used as a starting
point for new hint searches. The approach is interesting, but it represents
already existent and well developed theorem provers.
Even if not strictly part of the \hbugs{} architecture, the graphical user
- interface (GUI) of our prototype needs a lot of improvement if we would like
- it to be really usable by novices. In particular, the user is too easily
- distracted by the tutor's hints that are ``pushed'' to her.
+ interface (GUI) of our prototype needs a lot of improvement if we want
+ it to be really usable by novices. In particular, a critical issue
+ is avoiding continuous distractions for the user determined by the hints
+ that are asynchronously pushed to her.
Our \wss{} still lack a real integration in the MONET architecture,
since we do not provide the different ontologies to describe our problems,
projects / helm.git / blobdiff