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.