
TPTP
 Referenced in 383 articles
[sw04143]
 General guidelines outlining the requirements for ATP system evaluation. Standards for input and output ... support the testing and evaluation of ATP systems, to help ensure that performance results accurately ... ATP systems being considered. A common library of problems is necessary for meaningful system evaluations...

QMLTP
 Referenced in 8 articles
[sw09915]
 platform for testing and evaluating automated theorem proving (ATP) systems for firstorder modal logics...

MPTP 0.2
 Referenced in 45 articles
[sw02589]
 extended TPTP syntax, allowing a number of ATP experiments. This covers, for example, consistent handling ... Mizar schemes are now handled by the system, too, by remembering (and, if necessary, abstracting ... Mizar arithmetical evaluations. We describe several initial ATP experiments, both on the easy ... longer detected by the ATP systems, suggesting that the `Mizar deconstruction’ done by MPTP...

Proofwatch
 Referenced in 3 articles
[sw28654]
 design watchlistbased clause evaluation heuristics inside the E ATP system, and (ii) develop ... that load many previous proofs inside the ATP and focus the proof search using ... notion of proof matching. The methods are evaluated on a large set of problems coming...

PRocH
 Referenced in 12 articles
[sw10191]
 detailed inference steps recorded in the ATP (TPTP) proofs, using several internal HOL Light inference ... MESON tactic. The system is described and its performance is evaluated here on a large...

ACL2
 Referenced in 281 articles
[sw00060]
 ACL2 is both a programming language in which...

Coq
 Referenced in 1845 articles
[sw00161]
 Coq is a formal proof management system. It...

ILTP
 Referenced in 27 articles
[sw00437]
 The Intuitionistic Logic Theorem Proving (ILTP) library provides...

LEOII
 Referenced in 51 articles
[sw00512]
 LEOII is a standalone, resolutionbased higher...

Theorema
 Referenced in 146 articles
[sw00961]
 The software system Theorema provides a uniform logic...

TPS
 Referenced in 71 articles
[sw00973]
 TPS and ETPS are, respectively, the Theorem Proving...

ML
 Referenced in 517 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

SATLIB
 Referenced in 58 articles
[sw02107]
 SATLIB is a collection of benchmark problems, solvers...

OTTER
 Referenced in 316 articles
[sw02904]
 Our current automated deduction system Otter is designed...

THF0
 Referenced in 14 articles
[sw03310]
 THF0 is a syntactically conservative extension of the...

PETSc
 Referenced in 1240 articles
[sw04012]
 The Portable, Extensible Toolkit for Scientiﬁc Computation (PETSc...

CPLEX
 Referenced in 2665 articles
[sw04082]
 IBM® ILOG® CPLEX® offers C, C++, Java, .NET...

SMTLIB
 Referenced in 188 articles
[sw04103]
 SMTLIB was created with the expectation that...

CSPLib
 Referenced in 92 articles
[sw04150]
 CSPLib is a library of test problems for...

z3
 Referenced in 528 articles
[sw04887]
 Z3 is a highperformance theorem prover being...