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 Yazidi refugee problem domain.

Requirements

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:

• Treatment of equality is in an extremely naive from. That is, you can state in the KB exactly the equality and inequality clauses needed for the proof, Altenately, you may treat equality as a predicate, and add axioms like "for all x, x=x" and "not A=B" to the KB as needed.
• 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 need to implement the theorem, where the search component is done by the user: 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 resulting clause to the set of clauses. You will need to provide a reasonable interface for the user to do that - unless your program 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 simplified variant of Yazidi refugee problem from assignment 3. Do the following:

• Write out the set of axioms needed to perform causal reasoning for the domain, using situation calculus (that is, you do not need axioms that explain how is it that a certain vertex does not contain food, but you do need axioms that show that food at a vertex disappears when the agent arrives at the node).
• Convert them into a form your program can use (presumably, CNF).
• Write the goal to be proved in negated form.
• Use the program to derive a contradiction.

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

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: January 25, 2015.

In order to earn an independent bonus of up to 6% of the course grade, this assignment is to be submitted solo.