CS 4100 Artificial Intelligence
Spring 2012, Prof. Hafner
Assignments 4 and 5
Assigned: Feb 7, 2012

Assignment 4.  Due Feb. 14 as hard copy in class

A/B. Exercises 9.4 and 9.6 in  your textbook.  For exercise 9.6, use the "Isa" predicate for class membership.  For exercise 9.6, identify the logical elements you use in your logical sentences: the constants, the predicate symbols (with arity) and the function symbols, if any (with arity).

C. Convert the 6 kinship axioms from Section 8.3.2 of your textbook to a KB in Conjunctive Normal Form (CNF).  (Follow the procedure in the text and in the slides shown in class.  Show your work -- do not just give the final answer.)

D. Draw the AND/OR tree representing backward chaining for the knowledge base shown below for each of the two queries, AND SHOW WHAT ANSWER WOULD BE RETURNED by a backward chaining inference engine. (show all answers if there are more than one).  The format of the AND/OR tree is the “extended” format defined in class.

i.   Plays(?x, Basketball)
ii.  Is-happy(?x)
-----------------------------------------------------------------------------------------------------------
Knowledge base for Part D:

R1. Likes(x, Basketball) -> Plays(x, Basketball)
R2. Plays(x, Basketball) -> Is-healthy(x)  
R3. Has-pets(x) -> Is-happy(x)
R4. Is-healthy(x) and Is-rich(x) -> Is-happy(x)
F1. Likes(John, Basketball)
F2. Plays(Sam, Basketball)
F3. Is-rich(Sam)
F4. Has-pets(Sally)

Assignment 5.  Due Feb 21, by email 

The assignment is due at 10 pm on the due date, by email to saber@ccs.neu.edu.  The email must include an attachment of a zip file or tar file containing a folder named as in previous assignments: <your name>A5, 

Implement a backward chaining inference engine in python.  Your program MUST be in a source file named FOLBC.py.  It must include the following top-level functions:
	acquireKB(“KB file name”) 
	FOLBCtest(“queries file name”)

For each query, you are to perform backward chaining and print the answer in a readable form.  To accomplish this, FOLBCtest should do the following:
     a. read and echoes prints the next query
     b. call a function FOLBC with the query as an argument
     c. print the result of backward chaining in a human readable form

The core of your program will be a backward chaining function FOLBC(goal, theta). Goal is a list of FOLexp instances.  FOLBC returns a list of substitutions that will make the goal true. You are to use the FOLexp class provided to you to represent first order logic clauses. You are invited to use the unify.py program provided to you also.

A query will consist of an atomic formula as described below.  There will be one query per line in the queries input file.  To get full credit you should 
find and print ALL the correct answers to the query.  If there are no variables in the query then the answer will just be: Yes or No indicating that it was proved or not proved. The readability of your output will be part of your grade. Remember, no changes are made to the KB so each new query is independent of the previous queries.

The KB format will be as follows:
Atomic-formula
Atomic-formula IF Atomic-formula AND Atomic-Formula . . .  

"Facts" and "rules" may appear in any order in the file.

Example KB:
Likes[x, Pizza] IF Likes[x, Tomato] AND Likes[x,Cheese]
Likes[John, Cheese]
Likes[x, Pizza] IF Likes[Father[x], Pizza]
Likes[Father[Mary], Pizza]

Example queries:
Likes[z, Pizza]  (answer No)
Likes[Mary, Pizza]  (answer -- Yes)

Variables begin with lower case letters
Constants, predicate symbols and function symbols begin with upper case letters
Arguments are represented using Python's list format.

Some simple test files will be provided, but you should not depend on them to handle every case.