- Referenced in 383 articles
- 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...
- Referenced in 8 articles
- platform for testing and evaluating automated theorem proving (ATP) systems for first-order modal logics...
- Referenced in 45 articles
- 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...
- Referenced in 3 articles
- design watchlist-based 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...
- Referenced in 12 articles
- 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...
- Referenced in 281 articles
- ACL2 is both a programming language in which...
- Referenced in 1845 articles
- Coq is a formal proof management system. It...
- Referenced in 27 articles
- The Intuitionistic Logic Theorem Proving (ILTP) library provides...
- Referenced in 51 articles
- LEO-II is a standalone, resolution-based higher...
- Referenced in 146 articles
- The software system Theorema provides a uniform logic...
- Referenced in 71 articles
- TPS and ETPS are, respectively, the Theorem Proving...
- Referenced in 517 articles
- ML (’Meta Language’) is a general-purpose functional...
- Referenced in 58 articles
- SATLIB is a collection of benchmark problems, solvers...
- Referenced in 316 articles
- Our current automated deduction system Otter is designed...
- Referenced in 14 articles
- THF0 is a syntactically conservative extension of the...
- Referenced in 1240 articles
- The Portable, Extensible Toolkit for Scientiﬁc Computation (PETSc...
- Referenced in 2665 articles
- IBM® ILOG® CPLEX® offers C, C++, Java, .NET...
- Referenced in 188 articles
- SMT-LIB was created with the expectation that...
- Referenced in 92 articles
- CSPLib is a library of test problems for...
- Referenced in 528 articles
- Z3 is a high-performance theorem prover being...