The construction of a resolution proof using first-order logic

Question

I have the following review question for my upcoming exam that I would like to have some help with. I have to answer the query "Mary only uses green apples to make pies" using resolution. My current knowledge base and language is the following sentences:

Mary only uses apples from John to make pies:
 ∀π,a(Apple(a) ∧ Pie(π) ∧ Make(M,π,a) => Grows(J,a))
(⌐Apple(a) V ⌐Pie(π) V ⌐Make(M, π, a) V Grows(J,a))    (in CNF)

Latest update:

I will try to be more specific in general. The thing I want to prove is "Mary only uses green apples to make pies". Writing this logic I get:

Mary only uses green apples to make pies: π,a Pie(π) A Make(M, π, a) => Green(a)

And the steps in translating it into CNF form (http://en.wikipedia.org/wiki/Conjunctive_normal_form):

π,a ⌐(Pie(π) A Make(M, π, a)) V Green(a) 
π,a (⌐Pie(π) V ⌐Make(M, π, a)) V Green(a) 
(⌐Pie(π) V ⌐Make(M, π, a)) V Green(a) 
⌐Pie(π) V ⌐Make(M, π, a) V Green(a) (CNF form)

Negation of this statement in CNF form (Which we will use in the resolution for the proof):

Pie(π) A Make(M, π, a) A ⌐Green(a)

Now when using resolution for first order logic :(http://en.wikipedia.org/wiki/Resolution_(logic))

Is this right!? Or am I getting it wrong?

Answer 1

I'm not sure you're approaching the problem correctly. The first step is to encode the three statements ("Apples are either green or red", "John only grows green apples", "Mary only uses apples from John to make pies") into clausal form, which you haven't done.

The second step is to encode the negation of the statement you are trying to prove ("Mary only uses green apples to make pies") into clausal form as well. I don't think you've done that, I think you've encoded the positive statement. Perhaps I'm missing something. But encoding the query statement's negation ends up with four short statement strung together with ANDs, each of which can be treated as a statement in the knowledge base.

From there, the reduction is mechanical.

Update: Once again, you need to add the negation of the statement you are trying to prove. You're not doing that, you're adding the statement itself and another statement about the apples being green. Don't do that. You're not trying to prove a statement about the apples being green, you're trying to prove a statement about Mary only using green apples to make a pie. Negate that statement, resolve it with your three other knowledge base statements, and extract a contradiction (which is to say, resolve X and not-X together for some statement X.)

That is the algorithm. It works. If you don't do that, whether or not you "need" to, you're doing something other than the resolution algorithm, and were I grading your homework/exam, I'd grade it as incorrect.

Update 2: You're getting closer, but your query statement needs an additional clause about a being an Apple (i.e., Apple(a)) as several of your other statements already have. It should look almost exactly like the statement about Mary only using John's apples (and then negated because it is the query.) The form of it is correct, with the small clauses strung together with AND's, you're just missing one.

But then notice that once you do have that, each of those small clauses (because they are strung together with AND's) can act as an independent statement in your Knowledge Base. So for instance, the way you've formulated it right now, you could resolve Pie(p) with the expression for your third statement. There are a lot of steps in the resolution proof, but once you completely encode the query-negation, they are all tiny steps like that.

Answer 2

As a general information, you need to have your knowledge base in CNF, and a NEGATED goal (also in CNF). Then by unifying and applying resolution either you need to have a nil resolvent or the goal state itself. Other option is not being able to find any of these and resolve infinitely.

If

Make(p,π,a)

is in your knowledge base, then unifying and applying resolution it with the last resolvent which is:

⌐Make(M,π,a)

gives you a nil resolvent. At this point you can stop and conclude.