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.
Keywords for this software
References in zbMATH (referenced in 291 articles , 3 standard articles )
Showing results 1 to 20 of 291.
Sorted by year (- Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
- Benzmüller, Christoph: Cut-elimination for quantified conditional logic (2017)
- Gilbert, Frédéric: Proof certificates in PVS (2017)
- Gilbert, Frédéric: Automated constructivization of proofs (2017)
- Gleiss, Bernhard; Kovács, Laura; Suda, Martin: Splitting proofs for interpolation (2017)
- Itegulov, Daniyar; Slaney, John; Woltzenlogel Paleo, Bruno: Scavenger 0.1: a theorem prover based on conflict resolution (2017)
- Johansson, Moa: Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (2017)
- Maletzky, Alexander; Windsteiger, Wolfgang: The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema (2017)
- Parsia, Bijan; Matentzoglu, Nicolas; Gonçalves, Rafael S.; Glimm, Birte; Steigmiller, Andreas: The OWL reasoner evaluation (ORE) 2015 competition report (2017)
- Reynolds, Andrew; King, Tim; Kuncak, Viktor: Solving quantified linear arithmetic by counterexample-guided instantiation (2017)
- Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark: Constraint solving for finite model finding in SMT solvers (2017)
- Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam: Detecting inconsistencies in large first-order knowledge bases (2017)
- Sutcliffe, Geoff: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (2017)
- Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
- Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
- Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
- Ebner, Gabriel; Hetzl, Stefan; Reis, Giselle; Riener, Martin; Wolfsteiner, Simon; Zivota, Sebastian: System description: GAPT 2.0 (2016)
- Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei: Selecting the selection (2016)
- Khasidashvili, Zurab; Korovin, Konstantin: Predicate elimination for preprocessing in first-order theorem proving (2016)
- 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)