The TPTP World – Infrastructure for Automated Reasoning

  • Geoff Sutcliffe
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


The TPTP World is a well known and established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems for classical logics. The data, standards, and services provided by the TPTP World have made it increasingly easy to build, test, and apply ATP technology. This paper reviews the core features of the TPTP World, describes key service components of the TPTP World, presents some successful applications, and gives an overview of the most recent developments.


Classical Logic Automate Reasoning Proof Obligation World Knowledge Automate Theorem Prov 
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.
    Benzmüller, C., Paulson, L., Theiss, F., Fietzke, A.: LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  2. 2.
    Benzmüller, C., Rabe, F., Sutcliffe, G.: THF0 - The Core TPTP Language for Classical Higher-Order Logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 491–506. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  3. 3.
    Claessen, K., Sörensson, N.: New Techniques that Improve MACE-style Finite Model Finding. In: Baumgartner, P., Fermueller, C. (eds.) Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)Google Scholar
  4. 4.
    Cramer, M., Fisseni, B., Koepke, P., Kühlwein, D., Schröder, B., Veldman, J.: The Naproche Project: Controlled Natural Language Proof Checking of Mathematical Texts. In: Fuchs, N.E. (ed.) CNL 2009 Workshop. LNCS, vol. 5972, pp. 170–186. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Denney, E., Fischer, B., Schumann, J.: Using Automated Theorem Provers to Certify Auto-generated Aerospace Software. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 198–212. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Fuchs, N., Kaljurand, K., Kuhn, T.: Attempto Controlled English for Knowledge Representation. In: Baroglio, C., Bonatti, P.A., Małuszyński, J., Marchiori, M., Polleres, A., Schaffert, S. (eds.) Reasoning Web. LNCS, vol. 5224, pp. 104–124. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Hillenbrand, T.: Citius altius fortius: Lessons Learned from the Theorem Prover Waldmeister. In: Dahn, I., Vigneron, L. (eds.) Proceedings of the 4th International Workshop on First-Order Theorem Proving. Electronic Notes in Theoretical Computer Science, vol. 86.1, pp. 1–13 (2003)Google Scholar
  8. 8.
    Hurd, J.: First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In: Archer, M., Di Vito, B., Munoz, C. (eds.) Proceedings of the 1st International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports, pp. 56–68 (2003)Google Scholar
  9. 9.
    Nieuwenhuis, R.: The Impact of CASC in the Development of Automated Deduction Systems. AI Communications 15(2-3), 77–78 (2002)Google Scholar
  10. 10.
    Niles, I., Pease, A.: Towards A Standard Upper Ontology. In: Welty, C., Smith, B. (eds.) Proceedings of the 2nd International Conference on Formal Ontology in Information Systems, pp. 2–9 (2001)Google Scholar
  11. 11.
    Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  12. 12.
    Paulson, L., Susanto, K.: Source-level Proof Reconstruction for Interactive Theorem Proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 232–245. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Puzis, Y., Gao, Y., Sutcliffe, G.: Automated Generation of Interesting Theorems. In: Sutcliffe, G., Goebel, R. (eds.) Proceedings of the 19th International FLAIRS Conference, pp. 49–54. AAAI Press, Menlo Park (2006)Google Scholar
  14. 14.
    Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications 15(2-3), 91–110 (2002)zbMATHGoogle Scholar
  15. 15.
    Rudnicki, P.: An Overview of the Mizar Project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311–332 (1992)Google Scholar
  16. 16.
    Schulz, S.: E: A Brainiac Theorem Prover. AI Communications 15(2-3), 111–126 (2002)zbMATHGoogle Scholar
  17. 17.
    Sutcliffe, G.: SystemOnTPTP. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 406–410. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  18. 18.
    Sutcliffe, G.: Semantic Derivation Verification. International Journal on Artificial Intelligence Tools 15(6), 1053–1070 (2006)CrossRefGoogle Scholar
  19. 19.
    Sutcliffe, G.: The SZS Ontologies for Automated Reasoning Software. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics. CEUR Workshop Proceedings, vol. 418, pp. 38–49 (2008)Google Scholar
  20. 20.
    Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4), 337–362 (2009)CrossRefzbMATHGoogle Scholar
  21. 21.
    Sutcliffe, G., Benzmüller, C.: Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of Formalized Reasoning 3(1), 1–27 (2010)MathSciNetzbMATHGoogle Scholar
  22. 22.
    Sutcliffe, G., Benzmüller, C., Brown, C.E., Theiss, F.: Progress in the Development of Automated Theorem Proving for Higher-order Logic. In: Schmidt, R.A. (ed.) Automated Deduction – CADE-22. LNCS, vol. 5663, pp. 116–130. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  23. 23.
    Sutcliffe, G., Fuchs, M., Suttner, C.: Progress in Automated Theorem Proving, 1997-1999. In: Hoos, H., Stützle, T. (eds.) Proceedings of the IJCAI 2001 Workshop on Empirical Methods in Artificial Intelligence, pp. 53–60 (2001)Google Scholar
  24. 24.
    Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP Language for Writing Derivations and Finite Interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 67–81. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  25. 25.
    Sutcliffe, G., Seyfang, D.: Smart Selective Competition Parallelism ATP. In: Kumar, A., Russell, I. (eds.) Proceedings of the 12th International FLAIRS Conference, pp. 341–345. AAAI Press, Menlo Park (1999)Google Scholar
  26. 26.
    Sutcliffe, G., Suda, M., Teyssandier, A., Dellis, N., de Melo, G.: Progress Towards Effective Automated Reasoning with World Knowledge. In: Murray, C., Guesgen, H. (eds.) Proceedings of the 23rd International FLAIRS Conference. AAAI Press, Menlo Park (2010) (to appear)Google Scholar
  27. 27.
    Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications 19(1), 35–48 (2006)MathSciNetzbMATHGoogle Scholar
  28. 28.
    Sutcliffe, G., Suttner, C.B.: Evaluating General Purpose Automated Theorem Proving Systems. Artificial Intelligence 131(1-2), 39–54 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Trac, S., Puzis, Y., Sutcliffe, G.: An Interactive Derivation Viewer. In: Autexier, S., Benzmüller, C. (eds.) Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 3rd International Joint Conference on Automated Reasoning. Electronic Notes in Theoretical Computer Science, vol. 174, pp. 109–123 (2006)Google Scholar
  30. 30.
    Turing, A.: Computing Machinery and Intelligence. Mind 59(236), 433–460 (1950)MathSciNetCrossRefGoogle Scholar
  31. 31.
    Urban, J.: MPTP 0.2: Design, Implementation, and Initial Experiments. Journal of Automated Reasoning 37(1-2), 21–43 (2006)CrossRefzbMATHGoogle Scholar
  32. 32.
    Van Gelder, A., Sutcliffe, G.: Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 156–161. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  33. 33.
    Weidenbach, C., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P., Dimova, D.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) Automated Deduction – CADE-22. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Geoff Sutcliffe
    • 1
  1. 1.University of MiamiUSA

Personalised recommendations