1School of Computer Science, The University of Birmingham
Edgbaston, Birmingham B15 2TT, England 2Fachbereich Informatik (FB 14), Universität des Saarlandes
D-66041 Saarbrücken, Germany
1. Motivation
Our poster proposes an architecture for resource guided concurrent
mechanised deduction which is motivated by some findings in cognitive
science. Our architecture particularly reflects Hadamard's
"Psychology of Invention" and builds on Bundy's proof
planning idea [Bundy88].
2. System Architecture
The architecture (for further details see [BeJaKeSo99])
that we describe here allows a number of proof search
attempts to be executed in parallel. Each specialised subsystem may
try a different proof strategy to find the proof of a
conjecture. Hence, a number of different proof strategies
are used at the same time in the proof search. However, following all
the available strategies simultaneously would quickly consume the
available system resources consisting of computation time and memory
space.
In order to prevent this, and furthermore, to guide the proof
search, we developed and employ a resource management concept
in proof search. Resource management is a technique which distributes
the available resources amongst the available subsystems
(cf. [Zilberstein95]). Periodically, it assesses the state of the
proof search process, evaluates the progress, chooses a promising
direction for further search and redistributes the available resources
accordingly. If the current search direction becomes increasingly less
promising then backtracking to the previous points in the search space
is possible. Hence, only successful or promising
proof attempts are allowed to continue searching for a proof.
This process is repeated until a proof is found, or some other
terminating condition is reached. An important aspect of our
architecture is that in
each evaluation phase the global proof state is updated,
that is, promising partial proofs and especially solved subproblems
are reported to a special plan server that maintains the progress
of the overall proof search attempt. Furthermore, interesting
results may be communicated between the subsystems (for instance, an
open subproblem may be passed to a theorem prover that seems to be more
appropriate).
This communication is supported by the shells implemented
around the specialised problem solvers. The resource management
mechanism analyses the theorem and decides which subsystems, i.e.,
which provers, should be launched and what
proportion of the resources needs to be assigned to a particular
prover.
The mechanism is also responsible for restricting the amount of
information exchange between subsystems, so that not all of the resources
are allocated to the communication. The Figure to the right
demonstrates this concurrent resource management based proof planning
architecture. The involved planning agents are represented by PAn and
the ovals indicate the amount of resources assigned to them in each reasoning phase.
We argue that
the effect of resource management leads to a less brittle search technique which we call focused search.
Breadth-first search is robust in the sense that it is impossible to
miss a solution. However, it is normally prohibitively
expensive. Heuristic search may be
considered as the other extreme case: it is possible to go with modest
resources very deep in a search tree. However, the search is brittle
in that a single wrong decision may make it go astray and
miss a solution, independently of how big the allocated resources are.
Focused search can be considered as a
compromise -- it requires more resources than heuristic search,
but not as much as breadth-first search. As a result, a solution can
still be found even if the focus of the search is misplaced. Clearly,
more resources are necessary in the case of a bad than of a good
focus.
References
[BeJaKeSo99]
C. Benzmüller, M. Jamnik, M. Kerber and V. Sorge.
Towards concurrent resource managed deduction.
Technical Report CSRP-99-17, University of Birmingham, School of
Computer Science, 1999.
[Bundy88]
A. Bundy.
The Use of Explicit Plans to Guide Inductive Proofs.
Proc. of the CADE-9, volume 310 of
LNCS, 1988. Springer Verlag, Berlin, Germany.
[Zilberstein95]
S. Zilberstein.
Models of Bounded Rationality.
In AAAI Fall Symposium on Rational Agency, Cambridge,
Massachusetts, November 1995.
