
TPTP
 Referenced in 372 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 116 articles
[sw07047]
 harnesses external firstorder automatic theorem provers (ATPs) to discharge interactive proof obligations arising ... Satallax, the two most prominent higherorder ATPs, improving its performance on higherorder problems ... explore their usefulness, these ATPs are measured against firstorder ATPs and builtin Isabelle...

MPTP 0.2
 Referenced in 43 articles
[sw02589]
 current firstorder automated theorem provers (ATPs) (and vice versa) and to boost the development ... based, knowledgebased, and generally AIbased 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...

ILTP
 Referenced in 26 articles
[sw00437]
 testing and benchmarking automated theorem proving (ATP) systems for firstorder and propositional intuitionistic logic ... collections for firstorder 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...

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

HR
 Referenced in 29 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 16 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 24 articles
[sw06216]
 dynamic geometry software (DGS), automatic theorem provers (ATP), and a repository of geometrical constructions, figures...

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

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...

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 8 articles
[sw09915]
 testing and evaluating automated theorem proving (ATP) systems for firstorder 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 5 articles
[sw18721]
 Stateoftheart 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...

Proofwatch
 Referenced in 3 articles
[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...

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

ATPboost
 Referenced in 2 articles
[sw28626]
 learning premise selection in binary setting with ATP feedback. ATPboost is a system for solving ... sets of largetheory problems by interleaving ATP runs with stateoftheart machine...

JGXYZ
 Referenced in 1 article
[sw32309]
 JGXYZ: an ATP system for gap and glut logics. This paper describes an ATP system ... followed by use of an existing ATP system for FOL. A key feature of JGXYZ ... binary connectives in order to produce an ATP system for the logic. Experimental results from...