×

zbMATH — the first resource for mathematics

The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. (English) Zbl 1425.68381
Summary: This paper describes the TPTP problem library and associated infrastructure, from its use of Clause Normal Form (CNF), via the First-Order Form (FOF) and Typed First-order Form (TFF), through to the monomorphic Typed Higher-order Form (TH0). TPTP v6.4.0 was the last release prior to the introduction of the polymorphic Typed Higher-order Form, and thus serves as the exemplar. This paper summarizes the aims and history of the TPTP, documents its growth up to v6.4.0, reviews the structure and contents of TPTP problems, and gives an overview of TPTP-related infrastructure.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (2010) · Zbl 1211.68371
[2] Baumgartner, P.: SMTtoTPTP-A converter for theorem proving formats. In: Felty, A., Middeldorp, A. (eds.) Proceedings of the 25th International Conference on Automated Deduction, number 9195 in Lecture Notes in Computer Science, pp. 285-294. Springer (2015) · Zbl 06515513
[3] Benzmüller, C; Paulson, L, Quantified multimodal logics in simple type theory, Log. Univ., 7, 7-20, (2013) · Zbl 1334.03014
[4] Benzmüller, C; Sorge, V; Jamnik, M; Kerber, M, Combined reasoning by automated cooperation, J. Appl. Log., 6, 318-342, (2008) · Zbl 1162.68646
[5] Benzmüller, C., Paleo, B.W.: Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. In: Schaub, T. (ed.) Proceedings of the 21st European Conference on Artificial Intelligence, pp. 93-98 (2014) · Zbl 1366.03169
[6] Blanchette, J; Greenaway, D; Kaliszyk, C; Kühlwein, D; Urban, J, A learning-based fact selector for isabelle/HOL, J. Autom. Reason., 57, 219-244, (2016) · Zbl 1386.68149
[7] Blanchette, J., Paskevich, A.: TFF1: The TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) Proceedings of the 24th International Conference on Automated Deduction, number 7898 in Lecture Notes in Artificial Intelligence, pp. 414-420. Springer (2013) · Zbl 1381.68260
[8] Böhme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., Haehnle, R. (ed) Proceedings of the 5th International Joint Conference on Automated Reasoning, number 6173 in Lecture Notes in Artificial Intelligence, pp. 107-121 (2010) · Zbl 1291.68327
[9] Comaromi, J.P., Beall, J., Matthews, W.E., New, G.R.: Dewey Decimal Classification and Relative Index, 20th edn. Forest Press, Cinderford (1989)
[10] Denney, E., Fischer, B., Schumann, J.: Using automated theorem provers to certify auto-generated aerospace software. In: Rusinowitch, M., Basin, D. (eds.) Proceedings of the 2nd International Joint Conference on Automated Reasoning, number 3097 in Lecture Notes in Artificial Intelligence, pp. 198-212 (2004) · Zbl 1126.68563
[11] Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding industrial hardware verification problems into effectively propositional logic. In: Bloem, R., Sharygina, N. (eds.) Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design, pp. 137-144. IEEE Press (2010) · Zbl 1113.68093
[12] Gent, I., Walsh, T.: CSPLib: a benchmark library for constraints. In: Jaffar, J. (ed.), Proceedings of the 5th International Conference on the Principles and Practice of Constraint Programming, number 1713 in Lecture Notes in Computer Science, pp. 480-481. Springer (1999) · Zbl 1113.68095
[13] Höfner, P., Struth, G.: Automated reasoning in Kleene Algebra. In: Pfenning, F. (ed.) Proceedings of the 21st International Conference on Automated Deduction, number 4603 in Lecture Notes in Artificial Intelligence, pp. 279-294. Springer (2007) · Zbl 1184.68462
[14] Hoos, H., Stützle, T.: SATLIB: an online resource for research on SAT. In: Gent, I., van Maaren, H., Walsh, T. (eds.) Proceedings of the 3rd Workshop on the Satisfiability Problem, pp. 283-292. IOS Press (2000) · Zbl 0979.68128
[15] Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: The TPTP typed higher-order form with rank-1 polymorphism. In: Fontaine, P., Schulz, S., Urban, J. (eds.) Proceedings of the 5th Workshop on the Practical Aspects of Automated Reasoning, number 1635 in CEUR Workshop Proceedings, pp. 41-55 (2016) · Zbl 1211.68371
[16] Kaliszyk, C; Urban, J, Learning-assisted automated reasoning with flyspeck, J. Autom. Reason., 53, 173-213, (2014) · Zbl 1314.68283
[17] Kotelnikov, E., Kovacs, L., Voronkov, A.: A first class boolean sort in first-order theorem proving and TPTP. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Proceedings of the International Conference on Intelligent Computer Mathematics, number 9150 in Lecture Notes in Computer Science, pp. 71-86. Springer (2015) · Zbl 1417.68187
[18] Matuszek, C., Cabral, J., Witbrock, M., DeOliveira, J.: An introduction to the syntax and content of Cyc. In: Baral, C. (ed.) Proceedings of the 2006 AAAI Spring Symposium on Formalizing and Compiling Background Knowledge and Its Applications to Knowledge Representation and Question Answering, pp. 44-49 (2006) · Zbl 1162.68646
[19] McCune, W.W.: Otter 3.3 Reference Manual. Technical Report ANL/MSC-TM-263, Argonne National Laboratory, Argonne, USA (2003) · Zbl 0666.68091
[20] Narizzano, M., Pulina, L., Tacchella, A.: The QBFEVAL Web Portal. In: Fischer, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) Proceedings of the 10th European Conference on Logics in Artificial Intelligence, pp. 494-497 (2006) · Zbl 1334.03014
[21] Otten, J.: leanCoP 2.0 and ileancop 1.2: high performance lean theorem proving in classical and intuitionistic logic. In: Baumgartner, P., Armando, A., Dowek, G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning, number 5195 in Lecture Notes in Artificial Intelligence, pp. 283-291 (2008) · Zbl 1165.68467
[22] Paulson, L., Blanchette, J.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics, number 2 in EPiC, pp. 1-11 (2010) · Zbl 1211.68371
[23] Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, number 257 in CEUR Workshop Proceedings, pp. 61-70 (2007)
[24] Pelletier, FJ, Seventy-five problems for testing automatic theorem provers, J. Autom. Reason., 2, 191-216, (1986) · Zbl 0642.68147
[25] Phillips, J.D., Stanovsky, D.: Automated theorem proving in loop theory. In: Sutcliffe, G., Colton, S., Schulz, S. (eds.) Proceedings of the CICM Workshop on Empirically Successful Automated Reasoning in Mathematics, number 378 in CEUR Workshop Proceedings, pp. 42-53 (2008)
[26] Plaisted, DA, Non-Horn clause logic programming without contrapositives, J. Autom. Reason., 4, 287-325, (1988) · Zbl 0666.68091
[27] 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 (2006)
[28] Quaife, A, Automated deduction in von Neumann-bernays-godel set theory, J. Autom. Reason., 8, 91-147, (1992) · Zbl 0768.03005
[29] Raths, T; Otten, J; Kreitz, C, The ILTP problem library for intuitionistic logic—release v1.1, J. Autom. Reason., 38, 261-271, (2007) · Zbl 1113.68093
[30] American Mathematical Society. Mathematical Subject Classification. American Mathematical Society (1992) · Zbl 1003.68718
[31] Sutcliffe, G, Semantic derivation verification: techniques and implementation, Int. J. Artif. Intell. Tools, 15, 1053-1070, (2006)
[32] Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M., Voronkov, A. (eds.) Proceedings of the 2nd International Symposium on Computer Science in Russia, number 4649 in Lecture Notes in Computer Science, pp. 6-22. Springer (2007)
[33] 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, number 418 in CEUR Workshop Proceedings, pp. 38-49 (2008) · Zbl 0768.03005
[34] Sutcliffe, G, The TPTP problem library and associated infrastructure. the FOF and CNF parts, v3.5.0, J. Autom. Reason., 43, 337-362, (2009) · Zbl 1185.68636
[35] Sutcliffe, G.: The TPTP world - infrastructure for automated reasoning. In: Clarke, E., Voronkov, A. (eds.) Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, number 6355 in Lecture Notes in Artificial Intelligence, pp. 1-12. Springer (2010) · Zbl 1253.68292
[36] Sutcliffe, G; Benzmüller, C, Automated reasoning in higher-order logic using the TPTP THF infrastructure, J. Formaliz. Reason., 3, 1-27, (2010) · Zbl 1211.68371
[37] Sutcliffe, G., Fuchs, M., Suttner, C.: Progress in automated theorem proving, 1997-2001. In: Hoos, H., Stützle, T. (eds.) Proceedings of the IJCAI’01 Workshop on Empirical Methods in Artificial Intelligence, pp. 53-60 (2001) · Zbl 1113.68095
[38] Sutcliffe, G., Pelletier, F.J.: Hoping for the truth—a survey of the TPTP logics. In: Markov, Z., Russell, I. (eds.) Proceedings of the 29th International FLAIRS Conference, pp. 110-115 (2016) · Zbl 1113.68093
[39] Sutcliffe, G., Schulz, S.: The thousands of models for theorem provers (TMTP) model library - first steps. In: Konev, B., Schulz, S., Simon, L. (eds.) Proceedings of the 11th International Workshop on the Implementation of Logics, number 40 in EPiC Series in Computing, pp. 106-121. EasyChair Publications (2016)
[40] Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bjørner, N., Voronkov, A. (eds.) Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, number 7180 in Lecture Notes in Artificial Intelligence, pp. 406-419. Springer (2012) · Zbl 1352.68217
[41] 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.) Proceedings of the 3rd International Joint Conference on Automated Reasoning, number 4130 in Lecture Notes in Artificial Intelligence, pp. 67-81 (2006) · Zbl 1222.68373
[42] Sutcliffe, G; Suttner, C, The state of CASC, AI Commun., 19, 35-48, (2006) · Zbl 1112.68464
[43] Sutcliffe, G; Suttner, C; Pelletier, FJ, The IJCAR ATP system competition, J. Autom. Reason., 28, 307-320, (2002) · Zbl 1003.68718
[44] Sutcliffe, G; Suttner, CB, The TPTP problem library: CNF release v1.2.1, J. Autom. Reason., 21, 177-203, (1998) · Zbl 0910.68197
[45] Sutcliffe, G; Suttner, CB, Evaluating general purpose automated theorem proving systems, Artif. Intell., 131, 39-54, (2001) · Zbl 0996.68182
[46] Sutcliffe, G., Zimmer, J., Schulz, S.: Communication formalisms for automated theorem proving tools. In: Sorge, V., Colton, S., Fisher, M., Gow, J. (eds.) Proceedings of the Workshop on Agents and Automated Reasoning, 18th International Joint Conference on Artificial Intelligence, pp. 52-57 (2003)
[47] 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, volume 174 of Electronic Notes in Theoretical Computer Science, pp. 109-123 (2007) · Zbl 1278.68282
[48] Urban, J, MPTP 0.2: design, implementation, and initial experiments, J. Autom. Reason., 37, 21-43, (2006) · Zbl 1113.68095
[49] Urban, J; Rudnicki, P; Sutcliffe, G, ATP and presentation service for mizar formalizations, J. Autom. Reason., 50, 229-241, (2013) · Zbl 1260.68380
[50] Urban, J., Sutcliffe, G., Pudlak, P., Vyskocil, J.: MaLARea SG1: machine learner for automated reasoning with semantic guidance. In: Baumgartner, P., Armando, A., Dowek, G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning, number 5195 in Lecture Notes in Artificial Intelligence, pp. 441-456. Springer (2008) · Zbl 1165.68434
[51] Van Gelder, A., Sutcliffe, G.: Extending the tptp language to higher-order logic with automated parser generation. In: Furbach, U., Shankar, N. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning, number 4130 in Lecture Notes in Artificial Intelligence, pp. 156-161. Springer (2006) · Zbl 1222.68375
[52] Verchinine, K., Lyaletski, A., Paskevich, A.: System for automated deduction (SAD): a tool for proof verification. In: Pfenning, F. (ed.) Proceedings of the 21st International Conference on Automated Deduction, number 4603 in Lecture Notes in Artificial Intelligence, pp. 398-403. Springer (2007) · Zbl 1213.68576
[53] Wisniewski, M., Steen, A., Benzmüller, C.: TPTP and beyond: representation of quantified non-classical logics. In: Benzmüller, C., Otten, J. (eds.) Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics, number 1770 in CEUR Workshop Proceedings, pp. 51-65 (2016) · Zbl 0910.68197
[54] Wos, LA; Overbeek, RA; McCharen, JD, Problems and experiments for and with automated theorem-proving programs, IEEE Trans. Comput., C-25, 773-782, (1976) · Zbl 0329.68075
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.