Automated theorem proving: the resolution method
Ronald Peikert · ACM SIGSAM Bulletin · 1987
The goal of this project is to learn the basic notions of predicate logic and of automated theorem proving. A small theorem prover written in LISP has been taken from [1] and can be used for this project. Knowledge of the programming language LISP is required only for the optional part of the project.