
Coq
 Referenced in 1784 articles
[sw00161]
 formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... semiinteractive development of machinechecked 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 welltyped ML program does...

HOL
 Referenced in 502 articles
[sw05492]
 which theorems can be proved and proof tools implemented. Builtin decision procedures and theorem...

Z
 Referenced in 278 articles
[sw10291]
 Using Z. Specification, refinement, and proof. The book is an indepth 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 higherorder 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 computerchecked 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 stateoftheart 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 proofcarryingcode 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...