p-SETHEO: Strategy Parallelism in Automated Theorem Proving
- 229 Downloads
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 such as time or the number of available processors enforce efficient use of these resources by partitioning them adequately among the involved strategies. One of the problems to be solved in the context of resource scheduling is an optimization problem. We describe this problem and discuss the prototypical theorem prover p-SETHEO.
KeywordsResource Schedule Model Elimination Automate Theorem Automate Theorem Prove Automate Deduction
Unable to display preview. Download preview PDF.
- 1.J. Avenhaus et al. Discount: A system for distributed equational deduction. RTA-6, 1995.Google Scholar
- 2.M. P. Bonacina, J. Hsiang. Distributed deduction by clause diffusion: The Aquarius prover. LNAI 722, Springer, 1993.Google Scholar
- 3.B. I. Dahn et al. Integration of Automated and Interactive Theorem Proving in ILF. CADE-14, 1997.Google Scholar
- 4.A. Geist et al. PVM: Parallel Virtual Machine. MIT Press, 1994.Google Scholar
- 5.M. Moser et al. Setheo and E-Setheo. The CADE-13 Systems. JAR, 18(2), 1997.Google Scholar
- 6.D. B. Sturgill, A. M. Segre. A Novel Asynchronous Parallelism Scheme for First-Order Logic. CADE-12, 1994.Google Scholar
- 7.G. Sutcliffe et al. The TPTP Problem Library. CADE-12, 1994.Google Scholar
- 8.Ch. Suttner, J. Schumann. Parallel Automated Theorem Proving. PPAI, Elsevier, 1993.Google Scholar