Note -- this is a replacement project for the one that was a MESS

If you wish to see the old one, it is here .

CMSC 421: Project 3
Oh yeah? Prove it! - TAKE 2

Due: Due Date - May 15, 2003 23:59:59

Late Policy:

The program will be accepted until May 18, 2003 at 23:59:59. Projects submitted between May 15 and May 18 will lose ONE FULL letter grade.
The project will not be accepted after 11:59:59 on May 18.

Goals of Project

Symbolic reasoning is one of the underlying pillars of Artificial Intelligence. The "purest" form of this is reasoning based on logic, and particularly theorem proving.

Your task is simple -- Really this time, I promise!!!

You will build a resolution thorem prover for PROPOSITIONAL logic and demonstrate it on several files.

What you must do -- EVERYONE

There is a well defined algorithm for propositional resolution which you can find the pseudo-code for here . This algorithm (which we will go over in class on May 6th) assumes that things are already in CNF form. You may make that assumption for this part.

You must implement this algorithm and demonstrate it on three problems (described below)

The format of the problem is that each line is a set of predicates that are one clause. The logic symbols *OR* and *AND* are the only ones we will use, negation will be indicated by a minus sign in front of a character, *AND* will only occur in conclusions. To make things easier, we will assume all propositions are a single alphabetical character. We will also use no input clauses with more than 3 variables (note that your resolver may have to create clauses which are larger). Thus the clause "A or B or C" would be written as

A *OR* B *OR* -C

The last clause in a file is the conclusion you need to prove -- remember you have to NEGATE it. To make it easier to recognize, it will begin with *THEREFORE*.

This is propositional logic, so there are NO variables or arguments.

These are the four files to demonstrate your program on.

As we will show in class, test files one and two have provable conclusions, test file 3 is not provable, test file 4, we're not telling.

Your program should not print out the result for every resolve2, but please make sure we can tell whenever something is added to new, and whether a proof is found (by more than saying 1 or 0).

extra credit

Do one of these