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 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).