WARNING -- WARNING --- DO NOT DO THIS PROJECT -- IT IS INCORRECT

Instead use The correct project 3

CMSC 421: Project 3
Oh yeah? Prove it!

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

Late Policy:

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 --in the book, Chapter 16, problem 16.4 (page 266) is an example of a little logic problem. You will write a program that can solve this problem, and can solve another problem (of our devising) which will be provided to you at a later point (near the submission date).

Some Details

You will not need to write a program that takes the Natural langauge directly, rather, it will start from an encoding of the problem. To make things easier, you will not need to handle the logic symbols, instead we will use some special terms:

Furthermore, you can assume that there is only one (1) matrix in any one (1) input statement, and that there may be zero (0) or one (1) prefix for that matrix. The Prefix will be identified by the symbol *Prefix* and the matrix by *Matrix*. The matrix will terminate with the symbol *End*

Therefore, a statement like "Every member of the Alpine Club is either a skier or a mountainclimber or both" could be written as:

*Prefix* *Forall* (x) *Matrix* MemberAlpineClub(x) *Implies* [ Skier(x) *Or* MountainClimber(x) ] *End*
The Last statement in the input file will be what needs to be proven, and it will start with the tag *Therefore*. The set of statements needed to do problem 16.4 can be found in this text file .

NOTES

  • Variables will be single lower case characters as in the example.
  • There will be no more than one (1) *Implies* per input.

    • Assignment

    You must be able to take as input a file like the one shown above and solve, by resolution, the statement in the *Therefore* returning a variable binding (extra credit, ALL variable bindings). You will need to produce an output that shows what your system does as follows:

    You will need to submit your homework with a trace of it solving a problem that will be released a couple of days before the assignment is due.

    Extra Credit 2

    A "real" theorem prover would need to work on more complex statements -- ones with more complex prefixes and matrices. For example, problem 16.10 uses a statement where one needs more than one of each. Extend your program to handle these sorts of problems, and demonstrate on 16.10 and/or other problem of complexity beyond

    Web Accessibility