**************************
* CPSC 625 - AI          *
* Project #2             *
* Due: Mon, Oct 23, 2006 *
**************************

The aim of this project is to implement a simple back-chaining theorem-prover
for propositional logic.  This will mainly involve: a) writing a parser that
can parse a standard representation of logic syntax for the knowledge base,
and b) writing the recursive back-chaining procedure to answer queries.  You
will need to be able to supply various knowledge bases consisting of a set of
rules and facts as input.  Your program should be able to take this file as
input.  Then your program should accept a query on the command line and return
True or False.

Here is the syntax we will use:

 <sentence> ::= <rule> | <fact>
 <fact> ::= <prop_sym> ::= any combination of letters, digits, or '_'
 <rule> ::= <prop_sym> (& <prop_sym)* -> <prop_sym>

In other words, it is a simple subset of propositional logic with only atomic
sentences or conjunctive rules.  Note, there is no disjunction or negation.
Use the symbol & for 'and' and the symbol '->' for implies.

Here is an example:

 in_house & muddy & weekend -> in_trouble
 in_house & loud -> in_trouble
 playing_game & homework_not_done & weekday -> in_trouble
 climb_on_tree -> in_trouble
 shouting -> loud
 playing_music -> loud
 saturday -> weekend
 sunday -> weekend
 monday -> weekday
 tuesday -> weekday
 in_house
 playing_music
 tuesday

Suppose your program is called 'prover', and you load it with this knowledge
base above called 'in_trouble.kb'.  Then we should be able to query it to
find out what is entailed:

unix prompt> prover in_trouble.kb
(read 10 rules and 3 facts)
OK

query? loud
True

query? playing_game
False

query? in_trouble
True

query? weekend
False

query? weekday
True

query? quit
Bye.

Be sure to include the check for the special case where a literal should
not be put on the goal stack if it is already on there.  Make sure your
program also works on the knowledge base on p. 220 in the textbook.

What to turn in
===============

There will be no written report for this project.  All you have to turn is a
hard-copy of your source code and some examples that show that it works.
(Feel free to make up knowledge bases of your for more interesting examples,
perhaps like something about rules for a robot in an home or office
environment.)  

You will also have to schedule time during the week of Oct 23-27 to meet with
me to run your code live for me to test it.  We must be able to log in to your
machine remotely from my office, or you may bring a laptop.