Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 4/2017

17.02.2017

The TPTP Problem Library and Associated Infrastructure

From CNF to TH0, TPTP v6.4.0

verfasst von: Geoff Sutcliffe

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Vorheriger Artikel The OWL Reasoner Evaluation (ORE) 2015 Competition Report

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
Seventh Framework Programme FP7/2007-2013, grant agreement PIIF-GA-2008-219982
 
2
NSF CI-EN grant 1405674: SystemOnTPTP - Online Services for Automated Theorem Proving in Classical Logic.
 
Literatur
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.
4.
Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined reasoning by automated cooperation. J. Appl. Log. 6(3), 318–342 (2008)CrossRefMATHMathSciNet
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)CrossRefMATHMathSciNet
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.
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.
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.
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.
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)CrossRefMATH
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)CrossRef
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)CrossRefMATHMathSciNet
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)MATHMathSciNet
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.
43.
Sutcliffe, G., Suttner, C., Pelletier, F.J.: The IJCAR ATP system competition. J. Autom. Reason. 28(3), 307–320 (2002)CrossRefMATH
44.
Sutcliffe, G., Suttner, C.B.: The TPTP problem library: CNF release v1.2.1. J. Autom. Reason. 21(2), 177–203 (1998)CrossRefMATH
45.
Sutcliffe, G., Suttner, C.B.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1–2), 39–54 (2001)CrossRefMATHMathSciNet
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)MATH
49.
Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229–241 (2013)CrossRefMATHMathSciNet
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)MATH
Metadaten
Titel
The TPTP Problem Library and Associated Infrastructure
From CNF to TH0, TPTP v6.4.0
verfasst von
Geoff Sutcliffe
Publikationsdatum
17.02.2017
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2017
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-017-9407-7

Premium Partner

    Bildnachweise