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 333 articles , 3 standard articles )
Showing results 1 to 20 of 333.
Sorted by year (- Lifschitz, Vladimir; Lühne, Patrick; Schaub, Torsten: Verifying strong equivalence of programs in the input language of \textscgringo (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)
- Claessen, Koen; Smallbone, Nicholas: Efficient encodings of first-order Horn formulas in equational logic (2018)
- Cristiá, Maximiliano; Rossi, Gianfranco: A set solver for finite set relation algebra (2018)
- Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
- Felty, Amy; Momigliano, Alberto; Pientka, Brigitte: Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions (2018)
- Gleiss, Bernhard; Kovács, Laura; Robillard, Simon: Loop analysis by quantification over iterations (2018)
- Jakubuv, Jan; Kaliszyk, Cezary: Towards a unified ordering for superposition-based automated reasoning (2018)
- Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A foolish encoding of the next state relations of imperative programs (2018)
- Lopez Hernandez, Julio Cesar; Korovin, Konstantin: An abstraction-refinement framework for reasoning with large theories (2018)
- Piotrowski, Bartosz; Urban, Josef: ATPboost: learning premise selection in binary setting with ATP feedback (2018)
- Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
- Steen, Alexander; Benzmüller, Christoph: The higher-order prover Leo-III (2018)
- Winkler, Sarah; Moser, Georg: Mædmax: a maximal ordered completion tool (2018)
- Benzmüller, Christoph: Cut-elimination for quantified conditional logic (2017)
- Gilbert, Frédéric: Automated constructivization of proofs (2017)
- Gilbert, Frédéric: Proof certificates in PVS (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)