• Coq

  • Referenced in 1890 articles [sw00161]
  • provides a formal language to write mathematical definitions, executable algorithms and theorems together with ... machine-checked proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert ... mathematics (e.g. the full formalization of the 4 color theorem or constructive mathematics at Nijmegen...
  • ML

  • Referenced in 522 articles [sw01218]
  • compiler writing, automated theorem proving and formal verification. (wikipedia...
  • UNITY

  • Referenced in 185 articles [sw13461]
  • obey and prove them as theorems using the formal specification. The methodology is illustrated through...
  • PVS

  • Referenced in 629 articles [sw03484]
  • theorem prover. It is intended to capture the state-of-the-art in mechanized formal...
  • Isar

  • Referenced in 144 articles [sw04599]
  • Theorem proving system supporting both interactive proof development and some degree of automation have become ... Isabelle. Despite this success in actually formalizing parts of mathematics and computer science, there ... semi-automated reasoning (Isar) approach to readable formal proof documents sets out to bridge ... given by state-of-the-art interactive theorem proving systems and an appropriate level...
  • ETPS

  • Referenced in 160 articles [sw06302]
  • extent under Windows. Potential applications of automated theorem proving include hardware and software verification, partial ... various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive ... intelligence. TPS can be used to prove theorems of first- and higher-order logic interactively ... ETPS: A System to Help Students Write Formal Proofs (postscript...
  • C-CoRN

  • Referenced in 36 articles [sw06752]
  • based library of constructive mathematics, formalized in the theorem prover Coq. Background: There ... mathematics on a computer in an active (formalized) way to see how one can interact ... which is a constructive theorem prover), but mainly because constructive mathematics has the additional bonus ... project, formalizing the Fundamental Theorem of Algebra. (See the history page for an overview...
  • Jordan

  • Referenced in 63 articles [sw23624]
  • formal proof of the Jordan curve theorem (60,000 lines of HOL Light proof scripts...
  • Matita

  • Referenced in 71 articles [sw06140]
  • pencil in italian) is an experimental, interactive theorem prover under development at the Computer Science ... software tool aiding the development of formal proofs by man-machine collaboration ... provides a formal language where mathematical definitions, executable algorithms and theorems cohexist, and an interactive...
  • Milawa

  • Referenced in 20 articles [sw09977]
  • have used the HOL4 theorem prover to formalize the logic of Milawa, prove the logic ... Lisp runtime. Our top-level HOL4 theorem states that when Milawa ... theorem is the most comprehensive formal evidence of a theorem prover’s soundness to date...
  • SymbolicData

  • Referenced in 28 articles [sw04621]
  • public repository of geometry theorem proof schemes Formalized proof schemes are the starting point ... testing, comparing, and benchmarking of different geometry theorem proving approaches and provers. To automatize such...
  • HOL Light

  • Referenced in 308 articles [sw06580]
  • Mike Gordon’s original HOL system. Theorem provers in this family use a version ... some non-trivial tasks in the formalization of mathematics and industrial formal verification...
  • Isabelle/ZF

  • Referenced in 63 articles [sw04973]
  • properties of computer languages and protocols. Isabelle/ZF formalizes the greater part of elementary set theory ... cardinals. Results proved include Cantor’s Theorem, the Recursion Theorem, the Schroeder-Bernstein Theorem ... Wellordering Theorem. Isabelle/ZF also provides theories of lists, trees, etc., for formalizing computational notions...
  • Flyspeck

  • Referenced in 123 articles [sw10277]
  • text as a narrative linked to the formal development. To make this possible ... mainly been used with the Coq theorem prover: we show that the system itself...
  • MPTP 0.2

  • Referenced in 50 articles [sw02589]
  • second version of the Mizar Problems for Theorem Proving (MPTP) system and first experimental results ... large formal Mizar Mathematical Library (MML) available to current first-order automated theorem provers (ATPs ... Mizar proof constructs into the TPTP formalism. The proofs using second-order Mizar schemes ... case already complete. About every fifth nonarithmetical theorem is proved in a fully autonomous mode...
  • MPTP

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

  • Referenced in 25 articles [sw06216]
  • that integrates dynamic geometry software (DGS), automatic theorem provers (ATP), and a repository of geometrical ... body of geometrical constructions and formally proven geometrical theorems. We believe that, with the help...
  • TPS

  • Referenced in 73 articles [sw00973]
  • extent under Windows. Potential applications of automated theorem proving include hardware and software verification, partial ... various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive ... intelligence. TPS can be used to prove theorems of first- and higher-order logic interactively...
  • OTTER

  • Referenced in 316 articles [sw02904]
  • deduction system Otter is designed to prove theorems stated in first-order logic with equality ... Otter is research in abstract algebra and formal logic. Otter and its predecessors have been...
  • E Theorem Prover

  • Referenced in 206 articles [sw10187]
  • Brainiac Theorem Prover: E is a theorem prover for full first-order logic with equality ... system will then try to find a formal proof for the conjecture, assuming the axioms...