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 363 articles , 3 standard articles )
Showing results 1 to 20 of 363.
Sorted by year (- Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
- Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark: Extending SMT solvers to higher-order logic (2019)
- Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
- Bhayat, Ahmed; Reger, Giles: Restricted combinatory unification (2019)
- Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
- Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel: On the generation of quantified lemmas (2019)
- Furbach, Ulrich; Krämer, Teresa; Schon, Claudia: Names are not just sound and smoke: word embeddings for axiom selection (2019)
- Li, Di Long; Tiu, Alwen: Combining proverif and automated theorem provers for security protocol verification (2019)
- Lifschitz, Vladimir; Lühne, Patrick; Schaub, Torsten: Verifying strong equivalence of programs in the input language of \textscgringo (2019)
- Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui: EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract) (2019) arXiv
- Rawson, Michael; Reger, Giles: Old or heavy? Decaying gracefully with age/weight shapes (2019)
- Reger, Giles; Voronkov, Andrei: Induction in saturation-based proof search (2019)
- Schulz, Stephan; Cruanes, Simon; Vukmirović, Petar: Faster, higher, stronger: E 2.3 (2019)
- Sternagel, Christian; Winkler, Sarah: Certified equational reasoning via ordered completion (2019)
- Stojanović-Ðurđević, Sana: From informal to formal proofs in Euclidean geometry (2019)
- Tammet, Tanel: GKC: a reasoning system for large knowledge bases (2019)
- Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe: Superposition for (\lambda)-free higher-order logic (2018)
- Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
- Charrier, Tristan; Pinchinat, Sophie; Schwarzentruber, François: Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment (2018)
- Claessen, Koen; Smallbone, Nicholas: Efficient encodings of first-order Horn formulas in equational logic (2018)