System description: Cooperation in model elimination: CPTHEO

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


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    S. E. Conry et al., DARES: A Distributed Automated Reasoning System. Proc. AAAI-90, pp. 78–85, 1990.Google Scholar
  2. 2.
    J. Denzinger. Knowledge-based distributed search using teamwork. ICMAS-95, AAAI-Press, pp. 81–88, 1995.Google Scholar
  3. 3.
    D. Fuchs. Coupling Saturation-Based Provers by Exchanging Positive/Negative Information. Proc. RTA-98, LNCS 1379, Springer, pp. 317–331, 1998.Google Scholar
  4. 4.
    M. Fuchs. Similarity-Based Lemma Generation for Model Elimination. Proc. FTP-97 Workshop, RISC-Linz Report Series No. 97-50, pp. 63–67, 1997.Google Scholar
  5. 5.
    M. Moser et al.. SETHEO and E-SETHEO. The CADE-13 Systems. JAR, 18(2), pp. 237–246, 1997.CrossRefGoogle Scholar
  6. 6.
    J. Schumann. DELTA — A Bottom-Up Preprocessor for Top-Down Theorem Provers. Proc. CADE-12, Springer, pp. 774–777, 1994.Google Scholar
  7. 7.
    G. Sutcliffe et al. The TPTP Problem Library. Proc. CADE-12, Springer, pp. 252–266, 1994.Google Scholar
  8. 8.
    C. Suttner, J. Schumann. Parallel Automated Theorem Proving. PPAI, Elsevier, pp. 209–257, 1993.Google Scholar
  9. 9.
    A. Wolf, M. Fuchs. Cooperative Parallel Automated Theorem Proving. Dynamic Load Distribution for Parallel Applications, Teubner, pp. 129–145, 1997.Google Scholar
  10. 10.
    A. Wolf, R. Letz. Strategy Parallelism in Automated Theorem Proving. Proc. FLAIRS-98 (to appear), 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Marc Fuchs
    • 1
  • Andreas Wolf
    • 1
  1. 1.Institut für InformatikTechnische UniversitÄt MünchenMünchen

Personalised recommendations