Introduction to Artificial Inteligence

Assignment B1 (Bonus assignment)

Resolution Theorem Prover


Constructing a partial resolution theorem proving program, and exercising it by using it to prove correctness of plans from the EU refugee problem domain.


The partial resolution theorem prover is a reduced version of a full-blown FOL resolution theorem prover. The input is a set of clauses, i.e. a formula in conjunctive normal form. The program should produce a proof that the formula is a contradiction. However, some simplifications are introduced in this assignment:

Note that you are expected to write your own unification algorithm and resolution code, not to use the internals of a logic programming language such as Prolog to do that. However, you can still get partial credit for the assignment, by implementing plan correctness checking, as required below.

In addition, you need to exercise your program on the simplified variant of EU refugee problem from assignment 3. Do the following:

You should show that your program works with at least 2 examples: the one from assignment 3, and the KB from the midterm quiz.


You need to turn in:

Deadline: January 17, 2016.

In order to earn an independent bonus of up to 5% of the course grade, this assignment is to be submitted solo. If submitted in pairs, you need to come up with a clear attribution between the submittors on how to divide the grade/bonus.