• 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 computer-checked 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 higher-order logic, intended ... proof tools and has been applied to some non-trivial 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 proof-assistance...
  • 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 Turing-complete formalism ... well-founded (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 higher-dimensional 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 Isabelle-classic 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...