Artificial Intelligence Assignments:

atp.lisp: Resolution Theorem Prover

Heuristic: length or # of clauses in an or statement Algorithm: A* search using length and cost of node.

Takes a knowledge base and a clause as input and will determine if that clause evelautates to be true or not based on the knowledge base. The program is written in lisp.