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 225 articles , 2 standard articles )

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

1 2 3 ... 10 11 12 next

  1. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  2. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
  3. Khasidashvili, Zurab; Korovin, Konstantin: Predicate elimination for preprocessing in first-order theorem proving (2016)
  4. Matsuzaki, Takuya; Iwane, Hidenao; Kobayashi, Munehiro; Zhan, Yiyang; Fukasaku, Ryoya; Kudo, Jumma; Anai, Hirokazu; Arai, Noriko H.: Race against the teens -- benchmarking mechanized math on pre-university problems (2016)
  5. Areces, Carlos; Orbe, Ezequiel: Symmetric blocking (2015)
  6. Baumgartner, Peter: SMTtoTPTP -- a converter for theorem proving formats (2015)
  7. Baumgartner, Peter; Bax, Joshua; Waldmann, Uwe: Beagle -- a hierarchic superposition theorem prover (2015)
  8. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
  9. Bury, Guillaume; Delahaye, David: Integrating simplex with tableaux (2015)
  10. Dang, Han-Hing; Möller, Bernhard B.: Extended transitive separation logic (2015)
  11. Dragan, Ioan; Kovács, Laura: Lingva: generating and proving program properties using symbol elimination (2015)
  12. Echenim, Mnacho; Peltier, Nicolas; Tourret, Sophie: Quantifier-free equational logic and prime implicate generation (2015)
  13. Furbach, Ulrich; Pelzer, Björn; Schon, Claudia: Automated reasoning in the wild (2015)
  14. Gorzny, Jan; Woltzenlogel Paleo, Bruno: Towards the compression of first-order resolution proofs by lowering unit clauses (2015)
  15. Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
  16. Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
  17. Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A first class Boolean sort in first-order theorem proving and TPTP (2015)
  18. Kühlwein, Daniel; Urban, Josef: MaLeS: A framework for automatic tuning of automated theorem provers (2015)
  19. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  20. Reger, Giles; Suda, Martin; Voronkov, Andrei: Playing with AVATAR (2015)

1 2 3 ... 10 11 12 next