• 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 semi-automated reasoning systems have an adequate ... given by state-of-the-art 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...
  • C-CoRN

  • Referenced in 35 articles [sw06752]
  • which is a constructive theorem prover), but mainly because constructive mathematics has the additional bonus ... exist. C-CoRN 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 first-order 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 ”First-Order 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 back-end 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 finite-dimensional; vector spaces ... Spence. The rank-nullity theorem generalises the existing development in the Archive of Formal Proof...
  • CSP-prover

  • 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 HOL-Complex. 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 resolution-based theorem prover for Horn-clause sentences. The restriction...