Automated Theorem Proving: Assignments
Using ATP Systems
Encoding and Solving a Problem
Implementing an ATP System, in Prolog