• Coq

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

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

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

  • Referenced in 594 articles [sw05492]
  • which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem...
  • Automath

  • Referenced in 414 articles [sw07127]
  • late sixties in order to represent mathematical proof in the computer. It’s the direct ... ancestor of the ”type theoretical” line of proof assistants from which the better known current...
  • ML

  • Referenced in 524 articles [sw01218]
  • ensures type safety – there is a formal proof that a well-typed ML program does...
  • Z

  • Referenced in 286 articles [sw10291]
  • Using Z. Specification, refinement, and proof. The book is an in-depth introduction ... further on in the book. Rather, most proofs are omitted and replaced by an appeal ... disappointment is that in those places where proofs are given, the treatment often is quite ... properties are not mentioned; many of the proofs about relational notions could have been given...
  • HOL Light

  • Referenced in 310 articles [sw06580]
  • overview. HOL Light is an interactive proof assistant for classical higher-order logic, intended ... logical kernel. Despite this, it provides powerful proof tools and has been applied to some...
  • Archive Formal Proofs

  • Referenced in 181 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 ... archive, looking at various properties of the proof developments, including size, dependencies, and proof style ... some insights into the nature of formal proofs...
  • ETPS

  • Referenced in 161 articles [sw06302]
  • facilities for searching for expansion proofs, translating these into natural deduction proofs, constructing natural deduction ... proofs, translating natural deduction proofs which do not contain cuts into expansion proofs, and solving ... facilities of TPS for constructing natural deduction proofs have been used under the name ETPS ... writing the appropriate lines of the proof and checking that the rules can be used...
  • Agda

  • Referenced in 207 articles [sw09689]
  • your code). Agda is also a proof assistant: It is an interactive system for writing ... checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics ... Löf. It has many similarities with other proof assistants based on dependent types, such...
  • E Theorem Prover

  • Referenced in 206 articles [sw10187]
  • will then try to find a formal proof for the conjecture, assuming the axioms ... proof is found, the system can provide a detailed list of proof steps that...
  • OTTER

  • Referenced in 320 articles [sw02904]
  • strategies for directing and restricting searches for proofs. Otter can also be used...
  • Isar

  • Referenced in 145 articles [sw04599]
  • Theorem proving system supporting both interactive proof development and some degree of automation have become ... systems have an adequate primary notion of proof that is amenable to human understanding ... automated reasoning (Isar) approach to readable formal proof documents sets out to bridge the semantic ... between internal notions of proof given by state-of-the-art interactive theorem proving systems...
  • INTOPT_90

  • Referenced in 306 articles [sw04705]
  • John conditions and computationally executed proofs of the existence of feasible points generalizing Hansen...
  • Pesca

  • Referenced in 164 articles [sw13664]
  • PESCA = Proof Editor for Sequent Calculus: Pesca is a program that helps in the construction ... proofs in sequent calculus. It works both as a proof editor and as an automatic ... theorem prover. Proofs constructed in Pesca can both be seen on the terminal and printed...
  • kepler98

  • Referenced in 195 articles [sw23625]
  • Proof of the Kepler Conjecture. The Kepler conjecture asserts that no packing of congruent balls ... code and other documentation for the 1998 proof of the Kepler Conjecture by Sam Ferguson...
  • VAMPIRE

  • Referenced in 264 articles [sw02918]
  • proved, the system produces a verifiable proof, which validates both the clausification phase...
  • AProVE

  • Referenced in 161 articles [sw07831]
  • AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. AProVE ... most powerful systems for automated termination proofs of term rewrite systems (TRSs ... completely flexible combination of different termination proof techniques. Due to this framework, AProVE...
  • Twelf

  • Referenced in 173 articles [sw06888]
  • TALT typed assembly language, a foundational proof-carrying-code system, and a type safety proof...