- 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
- 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.
- Formal Digital Library - A product of the PRL project and descendant of the Nuprl system, FDL is a system implemented in Common Lisp for developing, refining, and collecting formal proofs
- Hiper - High performance term rewriting E-completion system
- IMPS - IMPS is an Interactive Mathematical Proof System intended to provide organizational and computational support for the traditional techniques of mathematical reasoning
- Nuprl - A system for manipulating proofs based on the type theory of Martin-LÃ¶f
- opencyc - OpenCyc is the open software version of the Cyc knowledge base and reasoning engine - essentially a combination of Ontology, Common Sense Knowledge and containing hybrid heuristic and formal Theorem Provers, originally written to run on Symbolics machines, but later built on top of their own lisp core (itself implemented in CMUCL)
- Prolog Technology Theorem Prover - The Prolog Technology Theorem Prover 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
- Theorem Provers - Theorem Provers is a subtopic of AI
- TPS - TPS, standing for Theorem Proving System, is a theorem prover for first-order logic and type theory
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 utelize 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).