ProofPower
ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation.
|
NuPRL -
a theorem prover for program verification using a constructive type theory.
|
Coq -
a proof assistant for Coquand's Calculus of Constructions.
|
PVS
PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover.
|
Larch Prover
Larch is a multi-site project exploring methods, languages, and tools for the practical use of formal specifications.
Its prover, LP, is an interactive theorem proving system for multisorted first-order logic.
|
|
The Cambridge HOL system, an LCF-like proof tool for Higher Order Logic.
See also: Cambridge University Automated Reasoning Group
|
CLSI: Tarski's world, an educational proof tool for first order logic. |
Otter
Otter is designed to prove theorems stated in first-order logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs.
|
ACL2 -
Applicative Common Lisp, sucessor to the Boyer-Moore prover.
|
|