p-SETHEO: Strategy Parallelism in Automated Theorem Proving

  • Andreas Wolf
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


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.


Resource Schedule Model Elimination Automate Theorem Automate Theorem Prove Automate Deduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. Avenhaus et al. Discount: A system for distributed equational deduction. RTA-6, 1995.Google Scholar
  2. 2.
    M. P. Bonacina, J. Hsiang. Distributed deduction by clause diffusion: The Aquarius prover. LNAI 722, Springer, 1993.Google Scholar
  3. 3.
    B. I. Dahn et al. Integration of Automated and Interactive Theorem Proving in ILF. CADE-14, 1997.Google Scholar
  4. 4.
    A. Geist et al. PVM: Parallel Virtual Machine. MIT Press, 1994.Google Scholar
  5. 5.
    M. Moser et al. Setheo and E-Setheo. The CADE-13 Systems. JAR, 18(2), 1997.Google Scholar
  6. 6.
    D. B. Sturgill, A. M. Segre. A Novel Asynchronous Parallelism Scheme for First-Order Logic. CADE-12, 1994.Google Scholar
  7. 7.
    G. Sutcliffe et al. The TPTP Problem Library. CADE-12, 1994.Google Scholar
  8. 8.
    Ch. Suttner, J. Schumann. Parallel Automated Theorem Proving. PPAI, Elsevier, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Andreas Wolf
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMunich

Personalised recommendations