Strategy Parallelism in Automated Theorem Proving

May 1998

Proceedings of the Eleventh International Florida Artificial Intelligence Research Society Conference (FLAIRS 1998)

Volume

Proceedings of the Eleventh International Florida Artificial Intelligence Research Society Conference (FLAIRS 1998)

All Papers

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.