Scribd
Upload
179 views5 pages

Fol Inference 4 PDF

1. Resolution is a method for proving conclusions from premises expressed in first-order logic (FOL) by converting sentences to clause normal form and resolving clauses. 2. An example resolution proof shows Deep Blue is not intelligent from the premises that intelligent things have common sense and Deep Blue does not have common sense. 3. Another example uses resolution to prove Lulu is older than Fifi from the premises about Lulu and Fifi's relationship and properties of parents and their children.

Uploaded by

Saisha Chhabria
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
179 views5 pages

Fol Inference 4 PDF

1. Resolution is a method for proving conclusions from premises expressed in first-order logic (FOL) by converting sentences to clause normal form and resolving clauses. 2. An example resolution proof shows Deep Blue is not intelligent from the premises that intelligent things have common sense and Deep Blue does not have common sense. 3. Another example uses resolution to prove Lulu is older than Fifi from the premises about Lulu and Fifi's relationship and properties of parents and their children.

Uploaded by

Saisha Chhabria
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 5

Resolution in First-Order Logic

Basic steps for proving a conclusion S given


premises
Premise1, …, Premisen
(all expressed in FOL):

1. Convert all sentences to CNF

2. Negate conclusion S & convert result to CNF

3. Add negated conclusion S to the premise clauses

4. Repeat until contradiction or no progress is made:


a. Select 2 clauses (call them parent clauses)
b. Resolve them together, performing all required
unifications
c. If resolvent is the empty clause, a contradiction
has been found (i.e., S follows from the premises)
d. If not, add resolvent to the premises

If we succeed in Step 4, we have proved the


conclusion
Resolution Examples
Example 1:
• If something is intelligent, it has common sense
• Deep Blue does not have common sense
• Prove that Deep Blue is not intelligent
1. ∀x.I(x) ⇒ H(x) C1: ¬I(x) ∨ H(x)
2. ¬H(D) C2: ¬H(D)
Conclusion: ¬I(D)
Denial: C3: I(D) CNF

A resolution proof of ¬I(D):


¬I(x) ∨ H(x) ¬H(D)

{x/D}
¬I(D) I(D)

2nd literal,
Proof also written as: 1st clause
C4: ¬I(D) r[C1b, C2]
C5: r[C3, C4]
Resolution Examples (cont.)
Example 2:
Premises: Prove:
Mother(Lulu, Fifi) Older(Lulu, Fifi)
Denial:
Alive(Lulu)
¬Older(Lulu, Fifi)
∀x ∀y.Mother(x,y) ⇒ Parent(x,y)
∀x ∀y.(Parent(x,y) ∧ Alive(x)) ⇒ Older(x,y)

Mother(Lulu,Fifi) ¬Mother(x,y) ∨ Parent(x,y)


{x/Lulu,y/Fifi}

Parent(Lulu,Fifi) ¬Parent(x,y) ∨ ¬Alive(x) ∨ Older(x,y)


{x/Lulu,y/Fifi}

¬Alive(Lulu) ∨ Older(Lulu, Fifi) Alive(Lulu)

¬Older(Lulu, Fifi) Older(Lulu, Fifi)


Resolution Examples (cont.)
Example 3:
• Suppose the desired conclusion had been
“Something is older than Fifi”
∃x.Older(x, Fifi)
• Denial:
¬∃x.Older(x, Fifi)
also written as: ∀x.¬Older(x, Fifi)
in clause form: ¬Older(x, Fifi)
• Last proof step would have been

C8: Older(Lulu,Fifi) C5’: ¬Older(x, Fifi)

{x/Lulu}

Don’t make mistake of first forming clause


from conclusion & then denying it:
• Conclusion:
∃x.Older(x, Fifi) Cannot unify
Lulu,C!!
clause form: Older(C, Fifi)
denial: ¬Older(C, Fifi)
Question-Answering
Example 1:
“Who is Lulu older than?”
• Prove that
“there is an x such that Lulu is older than x”
• In FOL form:
∃x.Older(Lulu, x)
• Denial:
¬∃x.Older(Lulu, x)
∀x.¬Older(Lulu, x)
in clause form: ¬Older(Lulu, x)
• Successful proof gives
{x/Fifi} [Verify!!]

Example 2:
“What is older than what?”
• In FOL form:
∃x ∃y.Older(x, y)
• Denial:
¬∃x∃y.Older(x, y)
in clause form: ¬Older(x, y)
• Successful proof gives
{x/Lulu, y/Fifi} [Verify!!]

You might also like