Classic-rtp: A classic Resolution Theorem Prover

A theorem prover written in Common Lisp. The prover implements classic resolution as described in the text books. Its main purpose is to allow students to experiment with resolution theorem proving.

Please download the following files: