Adaptive Parallel Search for Theorem Proving

May 1999

Proceedings of the Twelfth International Florida Artificial Intelligence Research Society Conference (FLAIRS 1999)

Volume

Proceedings of the Twelfth International Florida Artificial Intelligence Research Society Conference (FLAIRS 1999)

All Papers

Many of the artificial intelligence techniques developed to date rely on heuristic search through large spaces. Unfortunately, the size of these spaces and the corresponding computational effort reduce the applicability of otherwise novel and effective algorithms. Because automated theorem proversrely on heuristic search through the space of possible inferences, they are subject to the same difficulties. A number of parallel and distributed approaches to search have considerably improved the performance of the search process. Our goal is to develop an architecture that automatically selects parallel search strategies for a variety of search problems. We describe one such architecture realized in the Eureka system, which uses machine learning techniques to select the parallel search strategy for a given problem space. Although Eureka has successfully improved parallel search for problem solving and planning, parallelizing theorem proving systems introduces several new challenges. We investigate the application of the Eureka system to a parallel version of the Otter theorem prover and show results from a subset of Tptp library problems.