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 blocks world toy domain.


The partial resolution theorem prover is a reduced version of a full-blown FOL resolution theorem prover. The input is a formula in disjunctive 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 blocks world variant described below. Do the following:

In this variant, there is only one action type: PutOn(x, y), which puts block x on object y if both x and y are "clear", and otherwise does nothing. A block is clear just when there is no block on top of it. There is one basic situation-specific predicate: On(x, y, s), which means that x is on y in situation s. You MAY wish to define the Clear(x, s) predicate denoting that x is clear in situation x, but that is not a requirement. Predicate Block(x) denotes that x is a block, and if so, only one block can be on top of it - and it can only be on top of one object. Predicate Table(x) denotes that x is a table, which is an object that is ALWAYS "clear", i.e. has space for many blocks, but cannot be put on top of anything.

The example you should use is: a world with one table T, and 3 blocks, A, B, C (all constants). In situation S0, A is on B and B is on the table. C is also on the table. Show that A is on B which is on C, and C is on the table, as a result of the sequence of actions: PutOn(A,T), PutOn(B,C), PutOn(A,B).


You need to turn in:

Deadline: January 25, 2012.