UP
Automation of Reasoning net links
Generic Tools
Logical Frameworks - a logical framework is a formal meta-language for deductive systems.
Proof General - a generic Emacs interface for proof assistants
Isabelle Isabelle is a popular generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).
Prosper Proof and Specification Assisted Design
MetaPRL Generic successor to NuPRL
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.
HOL 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.
Bibliography - an extensive bibliography on automated reasoning provided by ORA Canada.
formal maths - 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

hol-info A mailing list for users of the Cambridge HOL proof system and other interested parties. Info, admin, subscriptions.... Archives.
qed Mailing list for those interested in an ambitious project to mechanise mathematics. Messages to qed@mcs.anl.gov, subscription requests to qed-request. The mailing list is maintained automatically by majordomo@mcs.anl.gov
ProofPower For ProofPower users and developers. Info, admin, subscriptions.... Archives.
Isabelle Larry Paulson's generic theorem prover heavily exploiting higher order resolution in a formal metalanguage.
isabelle-users@cl.cam.ac.uk, subscriptions at isabelle-users-request.
NQTHM Otherwise known as the "Boyer-Moore" theorem prover. A list for users: nqthm-users@cli.com. Info and subscription requests to majordomo@cli.com.
MIT theorem provers list. A mailing list for information about theorem provers Information only, not a discussion group. Subscription requests to theorem-provers-request@mc.lcs.mit.edu


HOME UP © RBJ created 1995-10-8 modified 2004-12-8