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).
Pages in this topic: ACL2 cl-cudd DTP Prover Epilog System and Episodic Logic Formal Digital Library Hiper IMPS Nuprl opencyc Prolog Technology Theorem Prover PVS Specification and Verification System SNARK TPS
Also linked from: AI CLiki Bugs
CLiki pages can be edited by anyone at any time. Imagine a fearsomely comprehensive disclaimer of liability. Now fear, comprehensively