
Coq
 Referenced in 1906 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 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. Builtin 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 welltyped ML program does...

Z
 Referenced in 286 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 310 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...

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 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...

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 stateoftheart 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 proofcarryingcode system, and a type safety proof...