Planning for distributed theorem proving : The team work approach

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 independently with different heuristics on the problem. After a certain amount of time referees judge their results using the impact of the results on the behavior 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 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 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.