
Coq
 Referenced in 1880 articles
[sw00161]
 formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... development of machinechecked 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 welltyped 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 computerchecked 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 ... userlevel 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 ondemand 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, generalpurpose...

Matita
 Referenced in 71 articles
[sw06140]
 software tool aiding the development of formal proofs by manmachine 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 nontrivial 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 secondorder 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...