AUTHORS: Christoph Benzmueller(1), Mateja Jamnik(1),
Manfred Kerber(1), and Volker Sorge(2)
AFFILIATIONand ADDRESS:
(1) School of Computer Science
The University of Birmingham
Edgbaston, Birmingham B15 2TT
United Kingdom
(2) AG Deduktionsssteme
Fachbereich Informatik (FB 14)
Universitaet des Saarlandes
D-66041 Saarbruecken
Germany
E-Mail: C.E.Benzmuller@cs.bham.ac.uk, M.Jamnik@cs.bham.ac.uk,
M.Kerber@cs.bham.ac.uk, sorge@ags.uni-sb.de
TITLE: Resource Guided Concurrent Deduction
ABSTRACT:
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'' [Hadamard44]. In his study Hadamard describes the
predominant role of the unconsciousness when humans try to solve hard
mathematical problems. He explains this phenomenon by its most important
feature, namely that it can make (and indeed makes) use of concurrent
search (whereas conscious thought cannot be concurrent), see p. 22
[Hadamard44]: ``Therefore, we see that the unconscious has the important
property of being manifold; several and probably many things can and do
occur in it simultaneously. This contrasts with the conscious ego which
is unique. We also see that this multiplicity of the unconscious enables
it to carry out a work of synthesis.'' That is, in Hadamard's view, it
is important to follow different lines of reasoning simultaneously in
order to come to a successful synthesis.
For our system we therefore develop the notion of focused search and
show that a reasoning system can be built as the cooperative collection
of concurrently acting specialised problem solvers (which are
encapsulated in agent shells). These reasoners typically perform well in
a particular problem domain. The system architecture that we describe
assesses the subgoals of a theorem and distributes them to the
specialised solvers that look the most promising. Furthermore it
allocates resources (above all computation time and memory) to the
specialised reasoners. This technique is referred to as resource
management. Each reasoner terminates its search for a solution of a
given subgoal when the solution is found or when it runs out of its
assigned resources. We argue that the effect of resource management
leads to a less brittle search technique which has some advantages over
the traditional search techniques such as breadth first or heuristic
search. A prototype of the proposed system architecture is currently
implemented in the OMEGA/MATHWEB framework.
Our work does not directly follow the long-term goal of building a
`complete mind'. However we think that we will encounter many of the
problems in our limited domain which will have to be solved in building
a complete mind. In particular a distinction between different levels,
reactive and deliberative modes, meta-level reasoning and so on, seems
to be very important in the wider context of mathematical reasoning,
maybe even feelings play a role. So we think that our work could be of
general interest and that we could benefit from the general work in the
area.
SHORT CV's: We all work in the area of automated reasoning
and have a particular interest in agent-oriented mathematical
reasoning. Please refer to the following web-pages for
further details:
http://www.ags.uni-sb.de/~chris/
http://www.cs.bham.ac.uk/~mxj/
http://www.cs.bham.ac.uk/~mmk/
http://www.ags.uni-sb.de/~sorge/