• TPTP

  • Referenced in 383 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...
  • SMT-LIB

  • 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 term-dependent 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 56 articles [sw04439]
  • benchmarks. Reads in problems in the standard .tptp file format of the TPTP problem...
  • LEO-II

  • Referenced in 51 articles [sw00512]
  • present LEO-II can cooperate with TPTP compliant first-order 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 52 articles [sw06849]
  • Satallax online at the System On TPTP website...
  • Darwin

  • Referenced in 26 articles [sw04175]
  • clausal logic. It accepts problems formulated in tptp or tme format, non-clausal 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 first-order TPTP language, adding the syntax for higher-order ... adaptation of existing infrastructure for processing TPTP format data, e.g., parsing tools, pretty-printing 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...
  • E-Darvin

  • Referenced in 20 articles [sw06852]
  • logic with equality. It accepts problems in tptp or tme syntax. Non-clausal 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 SMT-LIB 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 SMT-LIB 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...