• TPTP

  • Referenced in 329 articles [sw04143]
  • test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with ... comprehensive library of the ATP test problems that are available today, in order to provide ... utility to convert the problems to existing ATP systems’ formats. General guidelines outlining the requirements ... ATP system evaluation. Standards for input and output for ATP systems. The principal motivation...
  • Sledgehammer

  • Referenced in 101 articles [sw07047]
  • harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations arising ... Satallax, the two most prominent higher-order ATPs, improving its performance on higher-order problems ... explore their usefulness, these ATPs are measured against first-order ATPs and built-in Isabelle...
  • MPTP 0.2

  • Referenced in 39 articles [sw02589]
  • current first-order automated theorem provers (ATPs) (and vice versa) and to boost the development ... based, knowledge-based, and generally AI-based ATP methods. This version of MPTP switches ... extended TPTP syntax, allowing a number of ATP experiments. This covers, for example, consistent handling ... Mizar arithmetical evaluations. We describe several initial ATP experiments, both on the easy...
  • Gandalf

  • Referenced in 33 articles [sw10133]
  • Gandalf is an automated theorem proving (ATP) system. It proves theorems formulated in logic. Since ... logic is a pretty universal language, ATP systems such as Gandalf can prove theorems ... communications protocols. A new application area for ATP systems is the Semantic Web: a project ... participated in the yearly CASC competitions for ATP systems, with impressive results, see CASC...
  • MaLARea

  • Referenced in 40 articles [sw10278]
  • tools (now the E and the SPASS ATP systems) with a machine learning component...
  • ILTP

  • Referenced in 22 articles [sw00437]
  • testing and benchmarking automated theorem proving (ATP) systems for first-order and propositional intuitionistic logic ... collections for first-order and propositional intuitionistic ATP systems and tools for converting the problems ... input syntax of some existing intuitionistic ATP systems. It also includes information about currently available ... ATP systems for intuitionistic logic and their performance results on the problems in the ILTP...
  • HR

  • Referenced in 27 articles [sw10392]
  • theorems for testing automated theorem provers (ATPs), or smaller numbers of prime implicates, which represent ... TPTP library of test problems for ATP systems. HR is a Java program available...
  • SystemOnTPTP

  • Referenced in 15 articles [sw10408]
  • interface that allows an ATP problem to be easily and quickly submitted in various ways ... range of ATP systems. The interface uses a suite of currentty available ATP systems ... submitted to one or more of the ATP systems in sequence, or may be submitted...
  • MathWeb

  • Referenced in 18 articles [sw10293]
  • delegated to an automated theorem prover (ATP) by encoding them into its interface logic, simply ... most cases. Despite this seemingly ideal situation, ATPs are seldom actually used by people other...
  • GeoThms

  • Referenced in 22 articles [sw06216]
  • dynamic geometry software (DGS), automatic theorem provers (ATP), and a repository of geometrical constructions, figures...
  • PRocH

  • Referenced in 11 articles [sw10191]
  • imports in HOL Light proofs produced by ATPs on the recently developed translation ... Light and Flyspeck problems to ATP formats. PRocH combines several reconstruction methods in parallel ... detailed inference steps recorded in the ATP (TPTP) proofs, using several internal HOL Light inference...
  • HOLyHammer

  • Referenced in 18 articles [sw11553]
  • Hammer: online ATP service for HOL Light. HOL(y)Hammer is an online AI/ATP service...
  • Zap

  • Referenced in 8 articles [sw06823]
  • proving for software analysis Automated theorem provers (ATPs) are a key component that many software ... However, the basic interface provided by ATPs (validity/satisfiability checking of formulas) has changed little over ... desiderata for such an interface to an ATP, the logics (theories) that ... ATP for program analysis should support, and present how we have incorporated many of these...
  • QMLTP

  • Referenced in 7 articles [sw09915]
  • testing and evaluating automated theorem proving (ATP) systems for first-order modal logics. The main ... stimulate the development of new modal ATP systems and to put their comparison onto ... running comprehensive tests with existing modal ATP systems. In the presented version...
  • BliStrTune

  • Referenced in 3 articles [sw18721]
  • State-of-the-art automated theorem provers (ATPs) such as E allow a large number ... learning methods that invent strategies automatically for ATPs were proposed previously. One of them ... BliStr), a system for automated invention of ATP strategies. In this paper we introduce BliStrTune...
  • tptp2X

  • Referenced in 5 articles [sw10409]
  • TPTP format to formats used by existing ATP systems. 2) Applies various transformations to TPTP...
  • Proofwatch

  • Referenced in 1 article [sw28654]
  • automation by smarter internal guidance of the ATP systems. In particular, we (i) design watchlist ... based clause evaluation heuristics inside the E ATP system, and (ii) develop new proof guiding ... that load many previous proofs inside the ATP and focus the proof search using...
  • MinRMS

  • Referenced in 2 articles [sw26877]
  • tertiary structure, and catalyze similar reactions involving ATP. Shown the figure below is the user...
  • ATPboost

  • Referenced in 1 article [sw28626]
  • learning premise selection in binary setting with ATP feedback. ATPboost is a system for solving ... sets of large-theory problems by interleaving ATP runs with state-of-the-art machine...