Strategy Parallelism in Automated Theorem Proving

Andreas Wolf and Reinhold Letz

Automated theorem provers use search strategies. Unfortunately, there is no unique strategy which is uniformly successful on all problems. A combination of more than one strategy increases the chances of success. Limitations of resources as time or processors enforce efficient use of these resources by partitioning the resources adequately among the involved strategies. This leads to an optimization problem. We describe this problem for general search problems and discuss in more detail an application in automated theorem proving.


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.