• Coq

  • Referenced in 1784 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 945 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 606 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...
  • Automath

  • Referenced in 403 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 514 articles [sw01218]
  • ensures type safety – there is a formal proof that a well-typed ML program does...
  • HOL

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

  • Referenced in 278 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 288 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...
  • ETPS

  • Referenced in 153 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...
  • OTTER

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

  • Referenced in 304 articles [sw04705]
  • John conditions and computationally executed proofs of the existence of feasible points generalizing Hansen...
  • E Theorem Prover

  • Referenced in 191 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...
  • Archive Formal Proofs

  • Referenced in 152 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...
  • Isar

  • Referenced in 140 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...
  • Agda

  • Referenced in 182 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...
  • VAMPIRE

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

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

  • Referenced in 146 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...
  • kepler98

  • Referenced in 165 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...
  • Pesca

  • Referenced in 129 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...