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,
-RILEGGERE E CORREGGERE:
-
-// certainly non-optimal presentation and structure. There are also quite many
- typos
-/ English: lots of errors in the third-person conjugation of verbs (missing s),
- please correct them - I will not list all of them. Try to have a native
- English speaker read the paper.
-- Sessions 2 and 4 are too long, there are many repetitions.
-
-
ROBA SOSTANZIALE:
-// The work presented in this paper, however, is still in a preliminary stage
- and convincing, novel scientific aspects are hardly identifiable
- (vedi sotto "Possibili spunti")
-
-Possibili spunti:
-
-NO: H-Bugs is an improved realization of the O-Ants approach; the
- architecture of H-Bugs is superior to that of O-Ants and H-Bugs
- provides more or at least some improved functionalities.
YES: H-Bugs is simply an adaptation of a subset of the functionalities
of O-Ants to the MONET web-services/brokers approach.
-HHMM: The paper presents a case study with H-Bugs that gives novel insights or
-NO provides new evidence for the usefulness of systems like H-Bugs and
- O-Ants. (Because the title says ...: a case study this is what the
- reader first expects).
(ii) In the conclusion the authors admit that their work is rather
preliminary and that a real integration into the
provided? I was actually hoping to find some more client independent
modelings of tutor services. Since this seems to be not an issue it
raises the question what the benefits of a modeling of H-Bugs within the
- MONET web-services / brokers approach generally can be? Where is the
- abstraction that is typically achieved in service/broker modelings (see
- second paragraph in the Introduction)? If there is no abstraction
+ MONET web-services / brokers approach generally can be?
+
+ Where is the abstraction that is typically achieved in service/broker
+ modelings (see second paragraph in the Introduction)?
+
+ If there is no abstraction
achieved over the representation format for proofs used by HELM what
again is the difference to O-Ants: the main application of O-Ants
operates on the OMEGA proof datastructure; however it has been claimed
that the O-Ants architecture is independent from it and this has
recently been illustrated by applications of the system in other
settings (e.g. paper at MKM-1001, Festschrift-Siekmann).
-(iii) A proper evaluation of the case study is missing and the authors
- themselves mention proper assessment as future work. The claim that the
- tutor embodying the HELM-Search-Engine has effectively increased the
- productivity of users is not at all justified in the paper.
-
projects / helm.git / commitdiff