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:
- prover.lisp [written by Shaul Markovitch].
This is the main file and contains the resolution theorem prover.
- unify.lisp[Borrowed from Norvig and Russell].
The file contains the unify function and its auxilary functions.
- cnf.lisp [Borrowed from Russell and Norvig].
Contains the code to convert formula to cnf form.
- infix.lisp[borrowed from Norvig and Russell
who borrowed it from Mark Kantrowitz] This file is not necessary. Its main
purpose is to allow writting axioms and theorems in infix form.
- load-prover.lispLoads all the above files.
- test1.lgcA small list of axioms used for
testing the system.