• 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 first-order logic. The top ACL2...
  • Oyster

  • Referenced in 32 articles [sw19629]
  • Theorem proving and program synthesis with Oyster. Martin-Lö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 Gauss-Seidel algorithm. A convergence theorem is proved using nonsmooth analysis. Several numerical results...
  • Princess

  • Referenced in 23 articles [sw06872]
  • Theorem Proving in First-Order 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...