
Isar
 Referenced in 144 articles
[sw04599]
 Theorem proving system supporting both interactive proof development and some degree of automation have become ... range of people. Paradoxically, none of the existing semiautomated reasoning systems have an adequate ... given by stateoftheart interactive theorem proving systems and an appropriate level ... Isar/VM interpreter. Compared to existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings...

Java PathFinder
 Referenced in 123 articles
[sw07658]
 previous work in applying existing model checkers and theorem provers to real applications...

BRAID
 Referenced in 18 articles
[sw04311]
 finite group. By Riemann’s existence theorem, braid orbits of generating systems for G with...

Cogent
 Referenced in 14 articles
[sw01300]
 rely on automatic theorem provers. The existing theorem provers, such as Simplify, lack precise support...

TPTP
 Referenced in 384 articles
[sw04143]
 library of test problems for automated theorem proving (ATP) systems. The TPTP supplies ... utility to convert the problems to existing ATP systems’ formats. General guidelines outlining the requirements...

MPTP
 Referenced in 26 articles
[sw02489]
 possibilities for current theorem provers, that arise with the existence of large integral bodies ... makes the largest existing corpus of formalized mathematics available to theorem provers. MPTP (Mizar Problems...

WhyML
 Referenced in 25 articles
[sw09709]
 with the help of various existing automated and interactive theorem provers. To keep verification conditions...

CCoRN
 Referenced in 35 articles
[sw06752]
 which is a constructive theorem prover), but mainly because constructive mathematics has the additional bonus ... exist. CCoRN grew out of the FTA project, formalizing the Fundamental Theorem of Algebra...

E Theorem Prover
 Referenced in 198 articles
[sw10187]
 Brainiac Theorem Prover: E is a theorem prover for full firstorder logic with equality ... form “there exists an X with property P”), the latest versions can also provide possible...

FOL Fitting
 Referenced in 5 articles
[sw28611]
 book ”FirstOrder Logic and Automated Theorem Proving”. The formalization covers the syntax of first ... order logic, its semantics, the model existence theorem, a natural deduction proof calculus together with...

SEPIA
 Referenced in 7 articles
[sw21585]
 SEPIA combines model inference with interactive theorem proving. Existing proof corpora are modelled using state...

Speedith
 Referenced in 6 articles
[sw19455]
 program that plugs into existing general purpose theorem provers. This allows for seamless formal verification...

DisCo
 Referenced in 7 articles
[sw10393]
 based on the PVS theorem prover also exists, and a model checking backend based...

OpenGeoProver
 Referenced in 10 articles
[sw07179]
 Java for implementation of various Automated Geometry Theorem Provers. It can be used ... integrated into existing geometry tools. Of algebraic geometry theorem provers it implements...

Vector Spaces
 Referenced in 2 articles
[sw28662]
 spaces, sum of subspaces; the replacement theorem; existence of bases in finitedimensional; vector spaces ... Spence. The ranknullity theorem generalises the existing development in the Archive of Formal Proof...

CSPprover
 Referenced in 16 articles
[sw11465]
 Fixed Point Theorems are used for two purposes: (1) to prove the existence of fixed ... Prover is based on the generic theorem prover Isabelle, using the logic HOLComplex. Within...

GeoThms
 Referenced in 25 articles
[sw06216]
 that integrates dynamic geometry software (DGS), automatic theorem provers (ATP), and a repository of geometrical ... GeoThms users can easily use/browse through existing geometrical content and build new contents. In this ... geometrical constructions and formally proven geometrical theorems. We believe that, with the help...

UTPCalc
 Referenced in 2 articles
[sw22067]
 intended to supplant existing theorem prover or language transformation technology. The tool is designed...

HOL/SPIN
 Referenced in 24 articles
[sw02987]
 realtime bound for this convergence. This extends existing results to deal with the RIP standard ... which has complexities not accounted for in theorems about abstract versions of the protocol...

GHC
 Referenced in 43 articles
[sw23765]
 Clauses was born from the examination of existing logic programming languages and logic programming ... restriction of a resolutionbased theorem prover for Hornclause sentences. The restriction...