Introduction to Artificial Inteligence
Bonus Assignment
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 from the mid-term exam. 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.
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: June 13, 2001. Note - this is an individual
assignment. Credit for a (perfectly completed) assignment
is 10% of final grade added to the computed final
grade from mid-term exams and other assignments.