We present a new way to use planning in automated theorem proving by means of distribution. To overcome the problem that often subtasks of a problem cannot be detected a priori (which prevents the use of known planning and distribution techniques) we use the teamwork approach: A team of experts independently works on the problem with different heuristics. After a certain amount of time referees judge their results using the impact of the results on the behaviour of the experts. Then a supervisor combines the selected results to a new starting point.
The supervisor also selects the experts that will work on the problem in the next round. 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 in revising a plan. Experimental results show that this planning approach for the assignment of experts to a team enables the system to solve many different examples in an acceptable time with the same start configur ation and without any intervention by the user.
Generated: 29/10/99