System description: similarity-based lemma generation for model elimination

  • Marc Fuchs
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.
    O.L. Astrachan and D.W. Loveland. The Use of Lemmas in the Model Elimination Procedure. Journal of Automated Reasoning, 19(1):117–141, 1997.CrossRefMathSciNetGoogle Scholar
  2. 2.
    M. Fuchs. Controlled Use of Clausal Lemmas in Connection Tableau Calculi. AR-Report, AR-98-02, TU München.Google Scholar
  3. 3.
    M. Fuchs. Flexible proof replay with heuristics. In Proc. EPIA-97, LNAI 1323, pages 1–12. Springer, 1997.Google Scholar
  4. 4.
    R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning, (13):297–337, 1994.CrossRefMathSciNetGoogle Scholar
  5. 5.
    D.W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978.Google Scholar
  6. 6.
    R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8(2):183–212, 1992.CrossRefMathSciNetGoogle Scholar
  7. 7.
    S. Minton. Quantitative Results Concerning the Utility of Explanation-Based Learning. Artificial Intelligence, (42):363–391, 1990. Elsevier Science Publishers.Google Scholar
  8. 8.
    J. Schumann. Delta — a bottom-up preprocessor for top-down theorem provers. In Proc. CADE-12. Springer, 1994.Google Scholar
  9. 9.
    M.E. Stickel. A prolog technology theorem prover: Implementation by an extended prolog compiler. Journal of Automated Reasoning, 4:353–380, 1988.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

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

Personalised recommendations