Introduction to Artificial Inteligence

Resolution Theorem Prover

Goals

Constructing a partial resolution theorem proving program, and exercising it by using it to prove correctness of plans from the blocks world toy domain.

Requirements

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:

• Treatment of equality is in an extremely naive from. Equality is to be treated as a special predicate implemented by a special function. The function will evaluate to "true" if and only if the objects are the same constant name (e.g. A=A), where A is a constant.
• Define your own syntax variant such that you do not need to perform elaborate parsing. All input is already skolemized. Use any scheme you wish to separate out constants from variables.
• You do not need to implement the search component of the theorem prover. Do the proof semi-manually - the user specifies which clauses are to be resolved, and on which term. Your program only performs the unification and the resolution, and adds the result to the set of clauses. You will need to provide a reasonable interface for the user to do that - unless your progran can do the proof without user advice. (Full credit in either case, but I advise against this latter option, unless you have a LOT of extra time to spend!)

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:

• Write out the complete set of axioms for the domain, again using situation calculus.
• Convert them into a form your program can use.
• Write the goal to be proved in negated form.
• Use the program to derive a contradiction.

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).

Deliverables

You need to turn in:

• The program code and executable.
• The formulae used to axiomatize the domain, and the specific example, in FOL.
• The file containing the formulae for the specified example.
• A trace of the program run that produces the contradiction.
• In addition, you will need to demonstrate the program, as usual, to the grader. Be prepared to do some other problem instance on demand!

Deadline: December 29, 2002.