
CLAM
 Referenced in 39 articles
[sw19619]
 proof editor into a fully automatic theorem proving system...

OMRS
 Referenced in 39 articles
[sw03359]
 communication of mathematical services in distributed theorem proving and symbolic computation environments...

GEOTHER 1.1
 Referenced in 30 articles
[sw02842]
 GEOTHER (GEOmetry THeorem provER), a module of Epsilon, is an environment implemented by Dongming Wang ... Java for manipulating and proving geometric theorems. In GEOTHER a theorem is specified by means ... needed in order to manipulate and prove the theorem. From the specification, GEOTHER can automatically ... dragging, and saved as PostScript files; prove the theorem using any of the five algebraic...

ILTP
 Referenced in 26 articles
[sw00437]
 Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem...

MPTP
 Referenced in 23 articles
[sw02489]
 theorem provers. MPTP (Mizar Problems for Theorem Proving) is a system for translating the Mizar ... automated theorem provers, and for generating theorem proving problems corresponding to MML. The first version ... problems from complete proofs of Mizar theorems, and about 630000 problems from the simple...

Ivy
 Referenced in 30 articles
[sw10279]
 proved. The application is resolution/paramodulation automated theorem proving for firstorder logic. The top ACL2...

Oyster
 Referenced in 32 articles
[sw19629]
 Theorem proving and program synthesis with Oyster. MartinLöf type theory provides a formal framework...

jStar
 Referenced in 32 articles
[sw11261]
 verification system, called jStar, which combines theorem proving and abstract interpretation techniques. We demonstrate...

Analytica
 Referenced in 31 articles
[sw10478]
 Analytica is an automatic theorem prover for theorems in elementary analysis. The prover is written ... powerful symbolic computation system to prove theorems that are beyond the scope of previous automatic...

IsaPlanner
 Referenced in 29 articles
[sw02047]
 framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding ... used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that...

Lean
 Referenced in 28 articles
[sw15148]
 between interactive and automated theorem proving, by situating automated tools and methods in a framework...

SymbolicData
 Referenced in 27 articles
[sw04621]
 comparing, and benchmarking of different geometry theorem proving approaches and provers. To automatize such tests...

Transfer
 Referenced in 26 articles
[sw21009]
 build a library of operations and theorems about an abstract type, but they want ... packages: the Transfer package for proving theorems, and the Lifting package for defining constants...

Lifting
 Referenced in 26 articles
[sw21010]
 build a library of operations and theorems about an abstract type, but they want ... packages: the Transfer package for proving theorems, and the Lifting package for defining constants...

Epsilon
 Referenced in 39 articles
[sw00244]
 equations and inequations, and handle and prove geometric theorems automatically...

SIMEM3 Renault
 Referenced in 38 articles
[sw04243]
 block GaussSeidel algorithm. A convergence theorem is proved using nonsmooth analysis. Several numerical results...

Princess
 Referenced in 23 articles
[sw06872]
 Theorem Proving in FirstOrder Logic modulo Linear Integer Arithmetic. Princess is a theorem prover...

Isabelle/ZF
 Referenced in 62 articles
[sw04973]
 surjections, ordinals and cardinals. Results proved include Cantor’s Theorem, the Recursion Theorem, the Schroeder...

Nominal Isabelle
 Referenced in 68 articles
[sw12055]
 extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming...

iPiano
 Referenced in 45 articles
[sw09623]
 First, an abstract convergence theorem for a generic algorithm is proved, and then iPiano...