Higher-order Systems and Proof Checkers

- ACL2, from the University of Texas
- Coq Proof Assistant
- EVES, from ORA Canada
- HOL
- IMPS, an Interactive Mathematical Proof System
- Isabelle (a Generic Theorem Prover), from Cambridge University
- LEGO Proof Assistant
- Mizar, from the University of Bialystok
- Nqthm (Boyer-Moore Theorem Prover), from the University of Texas
- NuPrl, from Cornell
- ProofPower
- PVS (Prototype Verification System), from SRI International
- TPS, Carnegie Mellon University

- Bliksem
- DISCOUNT
- E
- E-SETHEO
- LeanTaP, a tableau-based theorem prover
- Gandalf
- LP, the Larch Prover
- METEOR, from Duke University
- OSHL, from the University of North Carolina
- Otter
- RRL, Rewrite Rule Laboratory
- SPASS, from MPI Saarbrücken
- Vampire
- Waldmeister

- Geometry Expert, from Wichita State University
- ILF (Integration of Logical Functions), from Humboldt University, Berlin

- TPTP , Thousands of Problems for Theorem Provers
- Schwerpunktprogramm Deduktion
- Logical Frameworks
- Formal Methods Library
- Database of Automated Reasoning Systems , by Carolyn Talcott
- Rewriting Page, by Nachum Dershowitz and Laurent Vigneron.

William McCune / mccune@mcs.anl.gov