The tableau-based theorem prover 3 T A P Version 4.0 | SpringerLink
Skip to main content
Springer Nature Link
Log in

The tableau-based theorem prover 3 T A P Version 4.0

  • Session 4B
  • Conference paper
  • First Online:
Automated Deduction — Cade-13 (CADE 1996)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1104))

Included in the following conference series:

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bernhard Beckert. A completion-based method for mixed universal and rigid E-unification. In A. Bundy, editor, Proceedings, 12th International Conference on Automated Deduction (CADE), Nancy, France, LNCS 814, pages 678–692. Springer, 1994.

    Google Scholar 

  2. Bernhard Beckert., Reiner Hähnle, Karla Geiß, Peter Oel, Christian Pape, and Martin Sulzmann. The many-valued tableau-based theorem prover 3TAP, version 4.0. Interner Bericht 3/96, Universität Karlsruhe, Fakultät für Informatik, 1996.

    Google Scholar 

  3. Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt. The even more liberalized δ-rule in free variable semantic tableaux. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Proceedings, 3rd Kurt Gödel Colloquium (KGC), Brno, Czech Republic, LNCS 713, pages 108–119. Springer, 1993.

    Google Scholar 

  4. Bernhard Beckert and Christian Pape. Incremental theory reasoning methods for semantic tableaux. In Proceedings, 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Palermo, Italy, LNCS. Springer. 1996.

    Google Scholar 

  5. Bernhard Beckert and Joachim Posegga. LeanT A P: Lean tableau-based deduction. Journal of Automated Reasoning, 15(3):339–358, 1995.

    Article  Google Scholar 

  6. Marcello D'Agostino, Dov Gabbay. Reiner Hähnle, and Joachim Posegga, editors. Handbook of Tableau Methods. Kluwer, Dordrecht, 1996. To appear.

    Google Scholar 

  7. Marcello D'Agostino and Marco Mondadori. The taming of the cut. Journal of Logic and Computation, 4(3), 1994.

    Google Scholar 

  8. Melvin C. Fitting. First-Order Logic and Automated Theorem Proving. Springer. 2nd edition, 1996.

    Google Scholar 

  9. Reiner Hähnle. Towards an efficient tableau proof procedure for multiple-valued logics. In Proceedings, Workshop on Computer Science Logic, Heidelberg, Germany, LNCS 533, pages 248–260. Springer, 1990.

    Google Scholar 

  10. Reiner Hähnle. Automated Deduction in Multiple-valued Logics, volume 10 of International Series of Monographs on Computer Science. Oxford University Press. 1994.

    Google Scholar 

  11. Reiner Hähnle and Werner Kernig. Verification of switch level designs with manyvalued logic. In A. Voronkov, editor, Proceedings, 4th International Conference on Logic Programming and Automated Reasoning (LPAR), St. Petersburg, Russia, LNCS 698, pages 158–169. Springer, 1993.

    Google Scholar 

  12. Reiner Hähnle and Peter H. Schmitt. The liberalized δ-rule in free variable semantic tableaux. Journal of Automated Reasoning, 13(2):211–222, 1994.

    Article  Google Scholar 

  13. Reinhold Letz. Klaus Mayr, and C. Goller. Controlled integration of the cut rule into connection tableau calculi. Journal of Automated Reasoning., 13(3):297–338, December 1994.

    Article  Google Scholar 

  14. F. Oppacher and E. Suen. HARP: A tableau-based theorem prover. Journal of Automated Reasoning, 4:69–100, 1988.

    Article  Google Scholar 

  15. Steve Reeves. Semantic tableaux as a framework for automated theorem-proving. In C. S. Mellish and J. Hallam, editors, Advances in Artificial Intelligence (Proceedings of AISB-87), pages 125–139. Wiley, 1987.

    Google Scholar 

  16. Wolfgang Reif. The KIV-system: Systematic construction of verified software. In Proceedings, 11th International Conference on Automated Deduction (CADE), Saratoga Springs, NY, USA, LNCS 607, pages 253–267. Springer, 1992.

    Google Scholar 

  17. Wolfgang Reif, Gerhard Schellhorn, and Kurt Stenzel. Interactive correctness proofs for software modules using KIV. In Proceedings, 10th Annual Conference on Computer Assurance (COMPASS), Washington, USA, pages 151–162, 1994.

    Google Scholar 

  18. Peter H. Schmitt. Computational aspects of three-valued logic. In J. H. Siekmann, editor, Proceedings, 8th International Conference on Automated Deduction (CADE), LNCS, pages 190–198. Springer, 1986.

    Google Scholar 

  19. Raymond M. Smullyan. First-Order Logic. Dover Publications, New York, second corrected edition, 1995. First published 1968 by Springer-Verlag.

    Google Scholar 

  20. Geoff Sutcliffe, Christian Suttner, and Theodor Yemenis. The TPTP problem library. In A. Bundy, editor, Proceedings, 12th International Conference on Automated Deduction (CADE). Nancy, France, LNCS 814, pages 708–722. Springer, 1994. Current version available on the World Wide Web at the URL http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/TPTP.HTML.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Logic, Complexity and Deduction Systems, University of Karlsruhe, Am Fasanengarten 5, 76128, Karlsruhe, Germany

    Bernhard Beckert, Reiner Hähnle, Peter Oel & Martin Sulzmann

Authors
  1. Bernhard Beckert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Reiner Hähnle
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Oel
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Martin Sulzmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

M. A. McRobbie J. K. Slaney

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beckert, B., Hähnle, R., Oel, P., Sulzmann, M. (1996). The tableau-based theorem prover 3 T A P Version 4.0. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_95

Download citation

  • DOI: https://doi.org/10.1007/3-540-61511-3_95

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61511-8

  • Online ISBN: 978-3-540-68687-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation