
TPTP
 Referenced in 381 articles
[sw04143]
 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 ... systems. The principal motivation for the TPTP is to support the testing and evaluation ... production of statistically significant results. The TPTP is such a library...

SMTLIB
 Referenced in 187 articles
[sw04103]
 same way as, for instance, the TPTP library has done for theorem proving...

Sledgehammer
 Referenced in 124 articles
[sw07047]
 variety of benchmarks from Isabelle and the TPTP library. Sledgehammer provides an ideal test bench...

MPTP 0.2
 Referenced in 45 articles
[sw02589]
 MPTP switches to a generic extended TPTP syntax that adds termdependent sorts and abstract ... Fraenkel) terms to the TPTP syntax. We describe these extensions and explain how they ... transformed by MPTP to standard TPTP syntax using relativization of sorts and deanonymization of abstract ... exported and also encoded in the extended TPTP syntax, allowing a number of ATP experiments...

Metis_
 Referenced in 53 articles
[sw04439]
 benchmarks. Reads in problems in the standard .tptp file format of the TPTP problem...

LEOII
 Referenced in 51 articles
[sw00512]
 present LEOII can cooperate with TPTP compliant firstorder automated theorem provers such ... CAML and its problem representation language is TPTP...

Nitpick
 Referenced in 61 articles
[sw00622]
 experimental results on Isabelle theories and the TPTP library indicate that Nitpick generates more counterexamples...

Satallax
 Referenced in 51 articles
[sw06849]
 Satallax online at the System On TPTP website...

Darwin
 Referenced in 25 articles
[sw04175]
 clausal logic. It accepts problems formulated in tptp or tme format, nonclausal tptp problems...

HR
 Referenced in 29 articles
[sw10392]
 production of benchmark theorems for the TPTP library of test problems for ATP systems...

THF0
 Referenced in 14 articles
[sw03310]
 conservative extension of the untyped ﬁrstorder TPTP language, adding the syntax for higherorder ... adaptation of existing infrastructure for processing TPTP format data, e.g., parsing tools, prettyprinting tools ... Section 5). A particular feature of the TPTP language, which has been maintained in THF0...

SystemOnTPTP
 Referenced in 16 articles
[sw10408]
 problem to be selected from the TPTP library or for a problem written in TPTP...

DCTP
 Referenced in 21 articles
[sw06621]
 input file containing the problem specification in TPTP syntax, DCTP will attempt to prove either...

EDarvin
 Referenced in 19 articles
[sw06852]
 logic with equality. It accepts problems in tptp or tme syntax. Nonclausal input...

DPPD
 Referenced in 14 articles
[sw09884]
 came up to generate something like the TPTP (Thousands of Problems for Theorem Proving) library...

PRocH
 Referenced in 12 articles
[sw10191]
 detailed inference steps recorded in the ATP (TPTP) proofs, using several internal HOL Light inference...

tptp2X
 Referenced in 5 articles
[sw10409]
 functional utility for reformatting, transforming, and generating TPTP problem files. In particular, it: 1) Converts ... from the TPTP format to formats used by existing ATP systems. 2) Applies various transformations ... TPTP problems. 3) Controls the generation of TPTP problem files from TPTP generator files. tptp2X...

SMTtoTPTP
 Referenced in 5 articles
[sw13650]
 format into the TPTP TFF format. The SMTLIB format supports polymorphic sorts and frequently ... arrays, and certain forms of arithmetics. The TPTP TFF format is an extension ... TPTP format widely used by automated theorem provers, adding a sort system and arithmetic theories ... making SMTLIB problems available to TPTP system developers, and for making TPTP systems available...

QMLTP
 Referenced in 8 articles
[sw09915]
 problems represented in a standardized extended TPTP syntax. Status and difficulty rating for all problems...

LeoPARD
 Referenced in 7 articles
[sw13554]
 LeoPARD include a parser for all TPTP dialects, a command line interpreter, and generic means...