Specific Tools

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.

Other Resources

Automated Reasoning Systems - a catalogue of AR systems maintained by Carolyn Talcot at Stanford. Argonne National Laboratory - aiming to develop techniques and build practical programs to help mathematicians, logicians, scientists, engineers, and others with some of the deductive aspects of their work. Home of Otter. - an extensive bibliography on automated reasoning provided by ORA Canada. - a page of links about tools supporting formal mathematical proof.

Automated Reasoning Group- at the Australian National University Combination Methods in Automated Reasoning - a page on combining different proof methods Stanford Logic Group The Automation of Proof A Historical and Sociological Exploration Theorem Proving Examples Simple examples of theorem proving code by John Harrison (for his book)

Some Mailing Lists