Manfred Kerber
15 July 1999
As an antithesis to this classical AI paradigm (and in particular to the planning paradigm) an approach has been developed that explicitly does not make use of knowledge representation and complicated deliberations (such as planning the best next step in the proof search). Brooks phrased it as ``Intelligence without Reason'' [8]. In this approach it is possible to obtain complex, apparently goal directed and intentional behaviour which has no long term internal state and no internal communication. This is referred to as a reactive form of modelling behaviour. Its key notions are: Situatedness (``The world is its own best model.''), embodiment (``The world grounds regress.''), Intelligence (``Intelligence is determined by the dynamics of interaction with the world.''), and Emergence (``Intelligence is in the eye of the observer.'').
Although the machine-oriented approaches were not designed in the light of recent work in reactive systems, they can be reinterpreted in this framework. The main aspect is the locality of the search for a solution. For instance, when we consider binary resolution theorem proving, the decision on which two literals to perform a resolution step is often made on the basis of the knowledge of the current proof state only. That is, it does not depend on what has been done previously (of course this view simplifies matters and is not true in a strict sense for all strategies). In particular, there is no overall long term strategy to derive the empty clause. We can view the behaviour of the theorem prover as a reactive process: the world consists of clauses and there is no abstract model of these clauses. The theorem prover acts directly in this world, and the behaviour is determined by the interaction with the world. It is a characteristic of reactiveness that some reactive systems such as normally do not do any backtracking. Furthermore, some reactive systems do complete restarts when the search for a proof is lost in the search space. Such restarts can also be viewed as a typical characteristic of reactive systems. For a detailed discussion of Brooks' approach and its relationship to theorem proving see [10].
Recent years have seen an attempt to reconcile the deliberative and the reactive approaches in single agent architectures [36]. This is partly motivated by looking at the human way of acting and reasoning which can be better explained as a combination of the two cases rather than by any one of them alone. Also, practical issues play an important rôle: in certain cases reactive behaviour is computationally more efficient, while in others reactive behaviour gets stuck. In the latter case deliberative behaviour can sometimes prevent blocking of a reasoning process.
A weakness of most state of the art reasoning systems is that they usually follow rigid and inflexible solution strategies in their search for proofs. Instead, human mathematicians use -- depending on their level of expertise -- ``a colourful mixture of proof strategies'' (as Wittgenstein phrases it). In an attempt to prove a mathematical theorem they typically first try a well known standard technique in the focus of the mathematical theory. If this technique does not lead to the wanted results in a reasonable amount of time, they may doubt that the theorem holds at all and look for a counterexample. If this also fails, they may try again by widening or deepening the proof search.
The aim of this research project is to emulate this flexible problem
solving behaviour of human mathematicians in an agent based reasoning
approach. Thus, our
system shall reflect at least some of the ideas of a sophisticated
and experienced problem solver as described by Pólya
in [34], p. 64: 
``when he does not succeed in guessing
the whole answer, he tries to guess some part of the answer, some
feature of the solution some approach to the solution, or some feature
of an approach to the solution. Then he seeks to expand his guess, and
so he seeks to adapt his guess to the best information he can get at
the moment.''
Agents allow a number of proof search attempts to be executed in parallel. Each agent 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 propose to develop and employ a resource management concept into proof search. Resource management is a technique which distributes the available resources amongst the available agents. Periodically, it assesses the state of the proof search process, evaluates the progress and redistributes the available resources accordingly. Hence, only successful or promising proof attempts will be allowed to continue searching for the proof. This process is repeated until the proof is found, or some other terminating condition is reached. Of course, the evaluation of the success of a proof strategy is crucial to determine the amount of resources that is allocated for an agent. This evaluation is based on the contribution that the agent has made in the proof attempt as well as on its prospect for the rest of the search. For example, a favourable contribution is a partial problem solution.
As will be illustrated below, the proposed system shall tackle mathematical problems that are currently not automatically solvable by any of the embedded systems alone (neither by any other system). In one particular example of [3] after splitting the initial proof goal into three subgoals, higher-order equality and extensionality reasoning is required. Whereas the first two subgoals can be solved by the higher-order prover [1], the third subproblem, which requires a fair amount of extensionality reasoning, should be solvable in a cooperation of the higher-order extensionality prover [4,2] with a first-order system like [37]. The system we propose shall be able to organise the required cooperation between the integrated systems in a goal oriented way in order to solve such kinds of problems automatically.
Classical first-order theorem provers (e.g. , , , ), analytical provers (e.g. or ), and completion methods (e.g. ) have reached a considerable reasoning power. This is underlined by the recent solution of the Robbins problem by [30]. However, these traditional systems follow fixed search strategies, which are unlikely to fully model the problem solving expertise of real mathematicians. Also classical higher-order theorem provers like [1], , or the -system [4,2] get lost in the enormous search spaces stretched on a fine-grained calculus level.
As an alternative approach Bundy developed proof planning [9], which instead of a fine-grained calculus level search looks for promising proof plans on a more abstract level by chaining proof methods. State of the art proof planner are , , and the proof planner of [7].
Agent architectures for automatic and interactive theorem proving are discussed in [16,14] and the preliminary work of the research fellow in this research field is described in [5,6].
An advantage of (which will form the basis of this project)
is that it already provides various integrated classical reasoning systems
(e.g. all the ones mentioned above) as well as
some specialised decision procedures (e.g. a constraint solver and
the integrated computer algebra systems Maple and
CAS [28]), and a basic analogy module [33].
Additional features are a multi-modal graphical user
interface [35], a proof verbalisation
tool [21] and a connected database of
mathematical theories.
Using the agent architecture [17], most of these
integrated system can be distributed over the internet.
Information on successful or unsuccessful proof attempts of the
integrated systems (e.g. partial proofs) can be translated back into
's central proof data structure, which is based
on a higher-order variant of Gentzen's natural deduction calculus.
Human proof search behaviour can best be modelled as a mixture of proof planning, classical theorem proving, computing, and model generation. In (and related systems like [12], which integrates only rather homogeneous first-order reasoning systems) this has mainly to be done by the user and rather poor support is provided for a fruitful and guided cooperation of the available subsystem. this weakness will be addressed in the proposed project. A particular problem of automated reasoning system is their ``brittleness'', that is, the feature that minor changes in the search strategy of in the problem formulation may totally change the behaviour of the system. The approach advocated in this proposal should at least partly remedy this problem, since by its explicit resource handling it enables explicit redirection of resources without abandoning lines of search altogether.
After consuming the available resources, the reasoning agents terminate
and investigate whether they have produced useful information or not.
For instance
the -agent could look for the shortest derived clauses
in order to estimate how close it is to a
proof. The contributions of the system,
which already returns a partial proof-plan to the -system, may be evaluated
using criteria like the complexity and number of the remaining open
subproblems (e.g. the only open subproblem might be a first-order goal
whereas the original problem was a higher-order one; then the partial
proof may be communicated to other systems and
the open subgoal can be passed to first-order provers).
Depending on the evaluation of the agents
contributions, a new resource distribution is computed.
 |
The most challenging research tasks are:
(i) The extension of 's underlying -architecture [17] by
suitable resource distribution and communication facilities. Whereas the
-architecture provides an excellent basis for distributing reasoning systems over
the Internet
it does not solve the question how to guide a fruitful co-operation between the involved
systems.
Therefore we want to adapt the blackboard mechanism
underlying 's interactive suggestion
mechanism [5,6].
(ii) The development and realisation of suitable evaluation criteria;
obvious candidates are the simplicity/complexity of partial proofs,
the theory/logic a subproblem belongs to (e.g. first-order logic,
set theory), or the similarity of open subproblems to already solved
problems stored in the database (note that already provides a basic
analogy component).
(iii) The extension of the system, such that it allows a grouping
of homogeneous agents tackling similar kinds of problems into one
single meta-agent. For instance, it may be useful to group
classical first-order reasoners
together to form a centre of expertise for classical first-order
logic. Optimally such centres of expertise may use an analogous mechanism
to the overall system to organise the communication between its
systems (sub-agents) and to further distribute the resources it
obtains at the upper level.
The systems in a centre of expertise can be evaluated
using more fine-grained evaluation criteria and more homogeneous
system communications can be realised.
In particular, for quite homogeneous (e.g. first-order) theorem provers experiments
of this kind have been successful (cf. the [14] or [16]).
The search for a proof of this theorem has not been automated yet. We indicate here how the proof might be found within our proposed architecture. First, the initial proof goal is split into three subgoals (e.g., with the help of a proof planner). Namely, from a given partition p we can derive the existence of an equivalence relation q, constituting subgoal (1). For the same equivalence relation q it holds that its equivalence classes are exactly p. The two directions of the set equality give us subgoals (2) and (3). Next, higher-order equality and extensionality reasoning is required. The first two subgoals (1) and (2) can be solved automatically by the higher-order prover [1]. The last subproblem (3), which requires a fair amount of extensionality reasoning, we expect to be solvable by cooperation between the higher-order extensionality prover [4] and a first-order automated theorem prover. provides the necessary higher-order extensionality treatment, however, it cannot cope with the large number of first-order clauses that are generated subsequently. Therefore, this set of clauses could be passed via to the first-order specialist available within our agent society. Our proposed system will be able to organise the sketched cooperation between the integrated systems in a goal oriented way in order to solve such kinds of problems automatically.
In contrast to former agent-based reasoning approaches (e.g. [14,38,13,12]) the proposed system focuses on the integration of quite heterogeneous systems (e.g. proof planner, higher-order prover, first-order prover, and model generators) on a more abstract communication layer.
MEGA.
:
Lovely 
User Interface.
This document was adapted from a file using the LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)
Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
The command line arguments were:
latex2html -split 0 epsrc-html.tex.
The translation was initiated by Manfred Kerber on 2001-03-28