
Isabelle/HOL
 Referenced in 1025 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 719 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...

Archive Formal Proofs
 Referenced in 181 articles
[sw28613]
 Formal Proofs is a vast collection of computerchecked proofs developed using the proof assistant ... various properties of the proof developments, including size, dependencies, and proof style. This gives some ... insights into the nature of formal proofs...

HOL Light
 Referenced in 310 articles
[sw06580]
 overview. HOL Light is an interactive proof assistant for classical higherorder logic, intended ... proof tools and has been applied to some nontrivial tasks in the formalization...

Isabelle/ZF
 Referenced in 64 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...

Ott
 Referenced in 32 articles
[sw00663]
 informal mathematics or the formal mathematics of a proof assistant  make it much harder than...

LEGO
 Referenced in 108 articles
[sw09685]
 interactive proof development system (proof assistant) designed and implemented by Randy Pollack in Edinburgh using ... interactive proof development in the natural deduction style. It supports refinement proof as a basic ... proofs. For example, features of the system like argument synthesis and universe polymorphism make proof ... more practical by bringing the level of formalization closer to that of informal mathematics...

MizarMode
 Referenced in 18 articles
[sw01973]
 MizarMode  an integrated proof assistance tool for the Mizar way of formalizing mathematics. The Emacs ... MizarMode and focuses on the proof assistance functions and tools available ... methods employed in tactical and programmable proof assistants, it makes the “proof code ... Proof Advisor, deductive tools like MoMM, etc. We give an overview of these proofassistance...

TacticToe
 Referenced in 6 articles
[sw28627]
 recently become an important component of formal proof assistants. Such ”hammer” tech niques complement traditional...

CoLoR
 Referenced in 38 articles
[sw09806]
 proof assistants. It is a very active subject of research in the Turingcomplete formalism ... wellfounded (rewrite) relations in the proof assistant Coq. We also present its application...

TRX
 Referenced in 9 articles
[sw08800]
 parser interpreter formally developed in the proof assistant Coq, capable of producing formally correct parsers...

Globular
 Referenced in 6 articles
[sw18031]
 article introduces Globular, an online proof assistant for the formalization and verification of proofs ... produces graphical visualizations of higherdimensional proofs, assists in their construction with a point ... allows hyperlinking of formalized proofs directly from research papers. It allows the formalization of proofs...

IsarMathLib
 Referenced in 3 articles
[sw22729]
 formalized mathematics for Isabelle/Isar proof assistant. In formalized mathematics definitions and proofs are written...

QuickChick
 Referenced in 5 articles
[sw13283]
 testing code can be formally verified using the proof assistant itself. In this work...

Isar
 Referenced in 145 articles
[sw04599]
 provides an interpreter for the Isar formal proof document language. Isabelle/Isar input consists either ... improper auxiliary commands (for diagnostics, exploration etc.). Proof texts consisting of proper document constructors only ... Theories, theorems, proof procedures etc. may be used interchangeably between Isabelleclassic proof scripts ... instantiation of Proof General, a generic (X)Emacs interface for interactive proof assistants, we arrive...

SAD
 Referenced in 15 articles
[sw09796]
 proof assistant called SAD is presented. SAD deals with mathematical texts that are formalized...

LNgen
 Referenced in 7 articles
[sw10111]
 carrying out such formalizations in the Coq proof assistant. As part of the presentation...

GeoCoq
 Referenced in 9 articles
[sw32242]
 library contains a formalization of geometry using the Coq proof assistant. It contains both proofs...

Gappa
 Referenced in 19 articles
[sw04885]
 tool intended to help verifying and formally proving properties on numerical programs dealing with floating ... automatic tactic for the Coq proof assistant...

Coquelicot
 Referenced in 13 articles
[sw11552]
 warranted in proof assistants, so that the users have a way to formally verify mathematical ... help with the proof process, the library comes with a comprehensive set of theorems that...