- ACL2 - ACL2 (A Computational Logic for Applicative Common Lisp) is a theorem prover for industrial Applications
- cl-cudd - CL-CUDD is a swig/cffi wrapper around the University of Colorado Decision Diagram library CUDD-2.4.2
- DTP Prover - DTP (Don's Theorem Prover) is "a sound and complete inference engine
- Epilog System and Episodic Logic - In contrast to Epilog Inference Package, the original Epilog system was created by Schubert, Hwang and Schaeffer for knowledge representation in Natural Language Processing, and is documented at the University of Rochester's Web
- Hiper - High performance term rewriting E-completion system
- IMPS - IMPS is an Interactive Mathematical Proof System developed by W
- Nuprl - The Nuprl system, based on the type theory of Martin-Löf, is a system for manipulating proofs
- OCML - The Operational Conceptual Modelling Language (OCML) combines logical reasoning in a frame-based language with the flexibility of extra-logical facilities like procedural attachment
- Prolog Technology Theorem Prover - The Prolog Technology Theorem Prover (PTTP) is an implementation (in Common Lisp) of the model elimination theorem-proving procedure that extends Prolog to the full first-order predicate calculus
- PVS Specification and Verification System - The PVS Specification and Verification System is a verification system: that is, a specification language integrated with support tools and a theorem prover
- SNARK - SNARK (SRI's New Automated Reasoning Kit) is described as "an automated theorem-proving program" being developed in Common Lisp
- TPS - TPS, standing for Theorem Proving System, is a theorem prover for first-order logic and type theory

Theorem Provers

Theorem Provers is a subtopic of AI. Many theorem provers are available in Common Lisp.
An important subarea of AI is Knowledge Representation. Knowledge Representation Systems that utilize some form of logic as the representation itself will come with some kind of theorem prover to operate on the logic (generally performing backward or forward chaining inference).