Abstract:
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.

Published Date: May 1998
Registration: ISBN 978-1-57735-051-4
Copyright: Published by The AAAI Press, Menlo Park, California