Adaptive Parallel Search for Theorem Proving

Diane J. Cook and Charles Hannon, University of Texas at Arlington

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.