Planning for distributed theorem proving:
The team work approach

Joerg Denzinger, Martin Kronenburg
Fachbereich Informatik, Universitaet Kaiserslautern
D-67663 Kaiserslautern, GERMANY
E-mail: {denzinge , kronburg}@informatik.uni-kl.de

Abstract
This paper presents a new way to use planning in automated
theorem proving by means of distribution. To overcome the problem
that often subtasks for a proof problem can not be detected a
priori which prevents the use of the known planning and
distribution techniques we use a team of experts that work with
different heuristics on the problem. After a certain time
referees judge their results using the impact of the results on
the behaviour of the expert and a supervisor combines the
selected results to a new starting point.

This supervisor also selects the experts that can work on the
problem. This selection is a reactive planning task. We outline
which information the supervisor can use to fulfill this task
and how this information is processed to result in a plan or to
revise a plan. We also show that the use of planning for the
assignment of experts to the team allows the system to solve
many different examples in an acceptable time with the same start
configuration and without any consultation of the user.

Keywords
automated theorem proving, distributed theorem proving, proof
planning, reactive planning

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1994/papers/
file: Kronenburg.SR-94-09.ps.Z