Automated Deduction Systems and Groups

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.