• Coq

  • Referenced in 1880 articles [sw00161]
  • formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... development of machine-checked proofs. Typical applications include the formalization of programming languages semantics...
  • Isabelle/HOL

  • Referenced in 1018 articles [sw01569]
  • generic proof assistant. It allows mathematical formulas to be expressed in a formal language ... main application is the formalization of mathematical proofs and in particular formal verification, which includes...
  • Isabelle

  • Referenced in 698 articles [sw00454]
  • generic proof assistant. It allows mathematical formulas to be expressed in a formal language ... main application is the formalization of mathematical proofs and in particular formal verification, which includes...
  • ML

  • Referenced in 522 articles [sw01218]
  • ensures type safety – there is a formal proof that a well-typed ML program does ... completely specified and verified using formal semantics. Its types and pattern matching make it well...
  • Archive Formal Proofs

  • Referenced in 178 articles [sw28613]
  • Isabelle’s Archive of Formal Proofs (AFP): Mining the Archive of Formal Proofs. The Archive ... Formal Proofs is a vast collection of computer-checked proofs developed using the proof assistant ... some insights into the nature of formal proofs...
  • Isar

  • Referenced in 144 articles [sw04599]
  • Theorem proving system supporting both interactive proof development and some degree of automation have become ... automated reasoning (Isar) approach to readable formal proof documents sets out to bridge the semantic ... user-level work. The Isar formal proof language has been designed to satisfy quite contradictory ... provides an interpreter for the Isar formal proof document language. Isabelle/Isar input consists either...
  • E Theorem Prover

  • Referenced in 198 articles [sw10187]
  • will then try to find a formal proof for the conjecture, assuming the axioms...
  • ETPS

  • Referenced in 160 articles [sw06302]
  • various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive ... facilities for searching for expansion proofs, translating these into natural deduction proofs, constructing natural deduction ... Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic Publishers, 2002. Descriptions ... System to Help Students Write Formal Proofs (postscript...
  • Flyspeck

  • Referenced in 121 articles [sw10277]
  • Communicating formal proofs: the case of flyspeck. We introduce a platform for presenting and cross ... linking formal and informal proof developments together. The platform supports writing natural language `narratives’ that ... formal text contains hyperlinks and gives on-demand state information at every proof step...
  • seL4

  • Referenced in 90 articles [sw15222]
  • knowledge, this is the first formal proof of functional correctness of a complete, general-purpose...
  • Matita

  • Referenced in 71 articles [sw06140]
  • software tool aiding the development of formal proofs by man-machine collaboration. It provides ... formal language where mathematical definitions, executable algorithms and theorems cohexist, and an interactive environment keeping ... current status of the proof, and updating it according to commands (usually called tactics) issued...
  • Jordan

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

  • Referenced in 307 articles [sw06580]
  • proof tools and has been applied to some non-trivial tasks in the formalization...
  • Z

  • Referenced in 282 articles [sw10291]
  • further on in the book. Rather, most proofs are omitted and replaced by an appeal ... formal specification and reasoning? Another disappointment is that in those places where proofs are given...
  • Isabelle/ZF

  • Referenced in 63 articles [sw04973]
  • generic proof assistant. It allows mathematical formulas to be expressed in a formal language ... main application is the formalization of mathematical proofs and in particular formal verification, which includes...
  • MPTP 0.2

  • Referenced in 50 articles [sw02589]
  • MPTP project is to make the large formal Mizar Mathematical Library (MML) available to current ... deanonymization of abstract terms. Full Mizar proofs are now exported and also encoded ... Mizar proof constructs into the TPTP formalism. The proofs using second-order Mizar schemes ... these cases, the newly discovered proofs are shorter than the MML originals and therefore...
  • SymbolicData

  • Referenced in 28 articles [sw04621]
  • repository of geometry theorem proof schemes Formalized proof schemes are the starting point for testing...
  • LEGO

  • Referenced in 107 articles [sw09685]
  • polymorphism make proof checking more practical by bringing the level of formalization closer to that...
  • CERES

  • Referenced in 21 articles [sw09442]
  • logic. The elimination of cuts in formal proofs corresponds to the removal of intermediate statements...
  • Featherweight Java

  • Referenced in 91 articles [sw16204]
  • give a detailed proof of type safety. The extended system formalizes for the first time...