Resolution Refutation
Resolution is one kind of proof technique that works this way - (i) select two clauses that contain
conflicting terms (ii) combine those two clauses and (iii) cancel out the conflicting terms.
For example we have following statements,
(1) If it is a pleasant day you will do strawberry picking
(2) If you are doing strawberry picking you are happy.
Above statements can be written in propositional logic like this -
(1) strawberry_picking ← pleasant
(2) happy ← strawberry_picking
And again these statements can be written in CNF like this -
(1) (strawberry_picking ∨~pleasant) ∧
(2) (happy ∨~strawberry_picking)
By resolving these two clauses and cancelling out the conflicting terms 'strawberry_picking'
and '~strawberry_picking', we can have one new clause,
(3) ~pleasant ∨ happy
When we write above new clause in infer or implies form, we have
'pleasant → happy' or 'happy ← pleasant'
i.e. If it is a pleasant day you are happy.
• But sometimes from the collection of the statements we have, we want to know the answer of this question -
"Is it possible to prove some other statements from what we actually know?“
• In order to prove this we need to make some inferences and those other statements can be shown true using
Refutation proof method i.e. proof by contradiction using Resolution.
• So for the asked goal we will negate the goal and will add it to the given statements to prove the
contradiction.
• Let's see an example to understand how Resolution and Refutation work. In below example,
• Part(I) represents the English meanings for the clauses,
• Part(II) represents the propositional logic statements for given english sentences,
• Part(III) represents the Conjunctive Normal Form (CNF) of Part(II) and
• Part(IV) shows some other statements we want to prove using Refutation proof method.
• Part(I) : English Sentences Part (II) : Propositional Statements
• (1) If it is sunny and warm day you (1) enjoy ← sunny ∧ warm
will enjoy.
• (2) If it is warm and pleasant day (2)strawberry_picking←warm ∧ pleasant
you will do strawberry picking
• (3) If it is raining then no (3) ~strawberry_picking ← raining
strawberry picking.
• (4) If it is raining you will get wet. (4) wet ← raining
• (5) It is warm day (5) warm
• (6) It is raining (6) raining
• (7) It is sunny (7) sunny
• Part(III) : CNF of Part(II)
• (1) (enjoy ∨~sunny∨~warm) ∧
• (2) (strawberry_picking ∨~warm∨~pleasant) ∧
• (3) (~strawberry_picking ∨~raining) ∧
• (4) (wet ∨~raining) ∧
• (5) (warm) ∧
• (6) (raining) ∧
• (7) (sunny)
• Why ∧ at the end of above statements?
• Part(IV) : Other statements we want to prove by Refutation
• (Goal 1) You are not doing strawberry picking.
• (Goal 2) You will enjoy.
• (Goal 3) Try it yourself : You will get wet.
• Conjunctive Normal Form (CNF):
• CNF is a particular way to write logical formulas. If logical formulas are written in
• 'conjunction' (i.e. clauses joined by and) then it is said to be in Conjunctive Normal
Form.
• You can see that Part(II) represents the propositional statements and Part(III) is a
CNF of Part(II).
• Any propositional statements can be transformed into conjunctive normal form
using and(∧) between the clauses.
• So, to convert the propositional statements into CNF, we write and between each
clause.
In our examples Part(II) has 7 statements. So, we will write these statements in
• CNF as below (1) and (2) and (3) and (4) and (5) and (6) and (7)
• Here and is replaced by ∧ to show them in conjunction of clauses (in CNF). Thus,
it will become (1) ∧ (2) ∧ (3) ∧ (4) ∧ (5) ∧ (6) ∧ (7)
Goal 2 : You will enjoy.
Goal 1 : You are not doing strawberry picking. Prove : enjoy
Prove : ~strawberry_picking
Assume : strawberry_picking (negate the goal and add it to given clauses). Assume : ~enjoy (negate the goal and add it to given
clauses)