More Web Proxy on the site http://driver.im/

article

The TPTP Problem Library and Associated Infrastructure

Author:

Geoff SutcliffeAuthors Info & Claims

Journal of Automated Reasoning, Volume 59, Issue 4

Pages 483 - 502

https://doi.org/10.1007/s10817-017-9407-7

Published: 01 December 2017 Publication History

Abstract

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.

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)

[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)

[3]

Benzmüller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Log. Univ. 7(1), 7---20 (2013)

[4]

Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined reasoning by automated cooperation. J. Appl. Log. 6(3), 318---342 (2008)

[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)

[6]

Blanchette, J., Greenaway, D., Kaliszyk, C., Kühlwein, D., Urban, J.: A learning-based fact selector for Isabelle/HOL. J. Autom. Reason. 57(3), 219---244 (2016)

Digital Library

[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)

[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)

[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)

[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)

[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)

[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)

[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)

[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)

[16]

Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173---213 (2014)

Digital Library

[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)

[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)

[19]

McCune, W.W.: Otter 3.3 Reference Manual. Technical Report ANL/MSC-TM-263, Argonne National Laboratory, Argonne, USA (2003)

[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)

[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)

[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)

[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, F.J.: Seventy-five problems for testing automatic theorem provers. J. Autom. Reason. 2(2), 191---216 (1986)

Digital Library

[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, D.A.: Non-Horn clause logic programming without contrapositives. J. Autom. Reason. 4(3), 287---325 (1988)

Digital Library

[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(1), 91---147 (1992)

Digital Library

[29]

Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic--release v1.1. J. Autom. Reason. 38(1---2), 261---271 (2007)

[30]

American Mathematical Society. Mathematical Subject Classification. American Mathematical Society (1992)

[31]

Sutcliffe, G.: Semantic derivation verification: techniques and implementation. Int. J. Artif. Intell. Tools 15(6), 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)

[34]

Sutcliffe, G.: The TPTP Problem library and associated infrastructure. The FOF and CNF Parts, v3.5.0. J. Autom. Reason. 43(4), 337---362 (2009)

Digital Library

[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)

[36]

Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1---27 (2010)

[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)

[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)

[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)

[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)

[42]

Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35---48 (2006)

Digital Library

[43]

Sutcliffe, G., Suttner, C., Pelletier, F.J.: The IJCAR ATP system competition. J. Autom. Reason. 28(3), 307---320 (2002)

Digital Library

[44]

Sutcliffe, G., Suttner, C.B.: The TPTP problem library: CNF release v1.2.1. J. Autom. Reason. 21(2), 177---203 (1998)

[45]

Sutcliffe, G., Suttner, C.B.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1---2), 39---54 (2001)

[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)

[48]

Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1---2), 21---43 (2006)

[49]

Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229---241 (2013)

Digital Library

[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)

[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)

[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)

[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)

[54]

Wos, L.A., Overbeek, R.A., McCharen, J.D.: Problems and experiments for and with automated theorem-proving programs. IEEE Trans. Comput. C---25(8), 773---782 (1976)

Cited By

Sutcliffe GDesharnais M(2024)The CADE-29 Automated Theorem Proving System Competition – CASC-29AI Communications10.3233/AIC-23032537:4(485-503)Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.3233/AIC-230325
Wernhard CBibel W(2024)Investigations into Proof StructuresJournal of Automated Reasoning10.1007/s10817-024-09711-868:4Online publication date: 29-Oct-2024
https://dl.acm.org/doi/10.1007/s10817-024-09711-8
From AJacobsen F(2024)Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-024-09697-368:3Online publication date: 27-Jun-2024
https://dl.acm.org/doi/10.1007/s10817-024-09697-3
Show More Cited By

The TPTP Problem Library and Associated Infrastructure

Recommendations

The TPTP Problem Library and Associated Infrastructure

This paper describes the First-Order Form (FOF) and Clause Normal Form (CNF) parts of the TPTP problem library, and the associated infrastructure. TPTP v3.5.0 was the last release containing only FOF and CNF problems, and thus serves as the exemplar. ...
The TPTP Problem Library

This paper provides a detailed description of the CNF part of the TPTP Problem Library for automated theorem-proving systems. The library is available via the Internet and forms a common basis for development and experimentation with automated theorem ...
The vampire and the FOOL
CPP 2016: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs

This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Automated Reasoning

Journal of Automated Reasoning Volume 59, Issue 4

December 2017

113 pages

ISSN:0168-7433

Issue’s Table of Contents

Copyright © Copyright © 2017 Springer Science+Business Media B.V.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 December 2017

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

56
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 06 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Sutcliffe GDesharnais M(2024)The CADE-29 Automated Theorem Proving System Competition – CASC-29AI Communications10.3233/AIC-23032537:4(485-503)Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.3233/AIC-230325
Wernhard CBibel W(2024)Investigations into Proof StructuresJournal of Automated Reasoning10.1007/s10817-024-09711-868:4Online publication date: 29-Oct-2024
https://dl.acm.org/doi/10.1007/s10817-024-09711-8
From AJacobsen F(2024)Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-024-09697-368:3Online publication date: 27-Jun-2024
https://dl.acm.org/doi/10.1007/s10817-024-09697-3
Almeida JFerreira Pires LGuizzardi GWagner G(2024)An Analysis of the Semantic Foundation of KerML and SysML v2Conceptual Modeling10.1007/978-3-031-75872-0_8(133-151)Online publication date: 29-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75872-0_8
Bártek FChvalovský KSuda M(2024)Regularization in Spider-Style Strategy Discovery and Schedule ConstructionAutomated Reasoning10.1007/978-3-031-63498-7_12(194-213)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_12
Heuer JWernhard C(2024)Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order LogicAutomated Reasoning10.1007/978-3-031-63498-7_11(172-193)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_11
Sutcliffe GDesharnais M(2023)The 11th IJCAR automated theorem proving system competition – CASC-J11AI Communications10.3233/AIC-22024436:2(73-91)Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.3233/AIC-220244
Limperg JFrom AKrebbers RTraytel DPientka BZdancewic S(2023)Aesop: White-Box Best-First Proof Search for LeanProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575671(253-266)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575671
Vukmirović PBlanchette JHeule M(2023)SAT-Inspired Eliminations for SuperpositionACM Transactions on Computational Logic10.1145/356536624:1(1-25)Online publication date: 18-Jan-2023
https://dl.acm.org/doi/10.1145/3565366
Liu PChen SLiu JXu YCao FWu G(2023)An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capabilityKnowledge-Based Systems10.1016/j.knosys.2022.110217261:COnline publication date: 15-Feb-2023
https://dl.acm.org/doi/10.1016/j.knosys.2022.110217
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents