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 multisite project exploring methods, languages, and tools for the practical use of formal specifications.
Its prover, LP, is an interactive theorem proving system for multisorted firstorder logic.


The Cambridge HOL system, an LCFlike 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 firstorder logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, KnuthBendix completion, weighting, and strategies for directing and restricting searches for proofs.

ACL2 
Applicative Common Lisp, sucessor to the BoyerMoore prover.

