Resource Guided Concurrent Deduction

C. Benzmüller1; M. Jamnik1; M. Kerber1; V. Sorge2

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.


© 2001, A K Peters. Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge
The URL of this page is
Also available as pdf ps.gz bib .