TPTP

The TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with: A comprehensive library of the ATP test problems that are available today, in order to provide an overview and a simple, unambiguous reference mechanism. A comprehensive list of references and other interesting information for each problem. Arbitrary size instances of generic problems (e.g., the N-queens problem). A utility to convert the problems to existing ATP systems’ formats. General guidelines outlining the requirements for ATP system evaluation. Standards for input and output for ATP systems. The principal motivation for the TPTP is to support the testing and evaluation of ATP systems, to help ensure that performance results accurately reflect capabilities of the ATP systems being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library.


References in zbMATH (referenced in 401 articles , 3 standard articles )

Showing results 1 to 20 of 401.
Sorted by year (citations)

1 2 3 ... 19 20 21 next

  1. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2021)
  2. Bromberger, Martin; Dragoste, Irina; Faqeh, Rasha; Fetzer, Christof; Krötzsch, Markus; Weidenbach, Christoph: A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (2021)
  3. Claessen, Koen; Lillieström, Ann: Handling transitive relations in first-order automated reasoning (2021)
  4. Cristiá, Maximiliano; Rossi, Gianfranco: Automated reasoning with restricted intensional sets (2021)
  5. Duarte, André; Korovin, Konstantin: AC simplifications and closure redundancies in the superposition calculus (2021)
  6. Ebner, Gabriel; Blanchette, Jasmin; Tourret, Sophie: A unifying splitting framework (2021)
  7. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
  8. Holden, Edvard K.; Korovin, Konstantin: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (2021)
  9. Otten, Jens: The \textsfnanoCoP2.0 connection provers for classical, intuitionistic and modal logics (2021)
  10. Proroković, Krsto; Wand, Michael; Schmidhuber, Jürgen: Improving stateful premise selection with transformers (2021)
  11. Rawson, Michael; Reger, Giles: Eliminating models during model elimination (2021)
  12. Rawson, Michael; Reger, Giles: \textsflazyCoP: lazy paramodulation meets neurally guided search (2021)
  13. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  14. Sutcliffe, Geoff: The 10th IJCAR automated theorem proving system competition -- CASC-J10 (2021)
  15. Sutcliffe, Geoff; Desharnais, Martin: The CADE-28 automated theorem proving system competition -- CASC-28 (2021)
  16. Vukmirović, Petar; Bentkamp, Alexander; Nummelin, Visa: Efficient full higher-order unification (2021)
  17. Wang, Qingxiang; Kaliszyk, Cezary: JEFL: joint embedding of formal proof libraries (2021)
  18. Zombori, Zsolt; Csiszárik, Adrián; Michalewski, Henryk; Kaliszyk, Cezary; Urban, Josef: Towards finding longer proofs (2021)
  19. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  20. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)

1 2 3 ... 19 20 21 next