Resolution and Planning

Due: Wednesday, November 9.

1. Given the following sentences, using a linear form proof, answer the question: Is John is happy? You will have to convert the sentences into implicitive or conjunctive normal form first, of course.

• Anyone passing his history exams and winning the lottery is happy.
• Anyone who studies or is lucky can pass all exams.
• John didn't study but is lucky.
• Anyone who is lucky wins the lottery.

You should use these predicates:

• pass(x,y) : "x passes the exam y"
• win(x) : "x wins the lottery"
• study(x) : "x studies"
• happy(x) : "x is happy"
• lucky(x) : "x is lucky"

2. Consider the following information:

1. Animals can outrun any animals that they can eat.
2. Carnivores eat other animals
3. Outrunning is transitive
4. Lions eat zebras
5. Zebras can outrun dogs
6. Dogs are carnivores

Use resolution theorem proving to find three animals that lions can outrun. You should review the concept of a skolem constant/function. For refutation you'll have to specify the negation of your desired conclusion. Consider that if your conclusion has a variable in it you may end up with multiple bindings for your proof. Those bindings should be the three animals.

 

3. Consider a STRIPS-like planner that is given the following set of operators:

BYPASS-EXAM:
precondition : Equal(grade, x)

add: Sleep-late, Equal(grade, x-10)

delete: Equal(grade, x)

TERM-PAPER:
precondition = Equal(grade, x)
add: Equal(grade, x+50)
delete: Equal(grade, x), Sleep-late

The planner is also given the axioms:

>=(grade, 80) iff Able-to-graduate

<(grade,80) iff ! Able-to-graduate

Devise a plan for the goal Able-to-graduate && Sleep-late, given Equal(grade,70). Show me the order in which the operators are executed, and how the working memory is manipulated each time. What is the conflict set at each step?