🌟 What is Resolution?
Resolution is a method used in logic to prove that a statement is true.
Instead of proving the statement directly, we:
👉 Assume the opposite (negation) is true
👉 Try to show this leads to a contradiction (false)
If it leads to a contradiction, then the original statement must be true.
How Resolution Refutation Works (Easy Steps)
1. Convert all statements into CNF
o CNF = Conjunctive Normal Form
o This means writing statements as combinations of ORs (∨) joined by ANDs
(∧).
2. Negate the conclusion
o Take the statement you want to prove.
o Assume it is false.
3. Add this negated conclusion to your given facts
4. Apply the resolution rule repeatedly
o Compare two clauses.
o Remove opposite literals (like P and ¬P).
o Create a new clause from what remains.
5. Stop when:
o ✅ You get a contradiction (empty clause → FALSE)
o ❌ Or no more steps are possible
What Does It Mean?
If you get a contradiction, the original statement is proved true.
If you cannot get a contradiction, then it cannot be proved using those facts.
What is Resolution Rule?
That’s the resolution step.
What is a Clause?
A clause is just:
A group of literals joined by OR (∨)
Example:
(P ∨ Q)
(¬P ∨ R ∨ S)
🔹 Conjunctive Normal Form (CNF) / Clause Normal Form
✅ Clause
A clause is:
A disjunction (OR) of one or more literals
A literal = a propositional variable (A, B, C…) or its negation (¬A, ¬B…)
Examples of clauses:
( A \vee B )
( \neg A \vee B \vee C )
( A ) (a single literal is also a clause)
✅ Conjunctive Normal Form (CNF)
A formula is in CNF if:
It is a conjunction (AND) of one or more clauses.
In short:
[
(\text{Clause}_1) \wedge (\text{Clause}_2) \wedge \dots \wedge (\text{Clause}_n)
]
Each clause contains only ORs of literals.
✔ Examples from the Image
These are in CNF:
1. [
\neg A \wedge (B \vee C)
]
2. [
(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E)
]
3. [
A \vee B
]
(This is valid because a single clause is allowed.)
4. [
A \wedge B
]
(This is valid because each literal itself is a clause.)
Good — let’s go very slowly and clearly.
I’ll convert both formulas to Clause Form step-by-step.
🔹 Formula 1
[
\forall x ; [Roman(x) \land know(x,Marcus)] \rightarrow hate(x, Caesar)
]
✅ Step 1: Remove Implication
Rule:
[
P \rightarrow Q \equiv \neg P \vee Q
]
So:
[
\forall x ; \neg [Roman(x) \land know(x,Marcus)] \vee hate(x, Caesar)
]
✅ Step 2: Remove Negation of AND
Rule (De Morgan’s Law):
[
\neg (A \land B) \equiv \neg A \vee \neg B
]
So:
[
\forall x ; [\neg Roman(x) \vee \neg know(x,Marcus) \vee hate(x, Caesar)]
]
✅ Step 3: Drop Universal Quantifier
In clause form, all variables are assumed universal, so we remove ∀x.
Final Clause:
[
\neg Roman(x) \vee \neg know(x,Marcus) \vee hate(x, Caesar)
]
✔ This is already a single clause (OR of literals).
🔹 Formula 2
[
\forall y ; \exists z ; hate(y,z) \rightarrow thinkcrazy(x,y)
]
⚠ First note: logically it should be:
[
\forall y ; \exists z ; (hate(y,z) \rightarrow thinkcrazy(x,y))
]
✅ Step 1: Remove Implication
[
\forall y ; \exists z ; [\neg hate(y,z) \vee thinkcrazy(x,y)]
]
✅ Step 2: Remove Existential Quantifier (Skolemization)
Since:
[
\exists z
]
depends on y, we replace z with a Skolem function of y:
[
z = f(y)
]
So we get:
[
\forall y ; [\neg hate(y,f(y)) \vee thinkcrazy(x,y)]
]
✅ Step 3: Drop Universal Quantifier
Remove ∀y.
Final Clause:
[
\neg hate(y,f(y)) \vee thinkcrazy(x,y)
]
🔹 Final Clause Set
1.
[
\neg Roman(x) \vee \neg know(x,Marcus) \vee hate(x, Caesar)
]
2.
[
\neg hate(y,f(y)) \vee thinkcrazy(x,y)
]
🔹 Why This Is Clause Form?
Because each statement is:
✔ A disjunction (OR)
✔ Of literals
✔ With no implication
✔ With no existential quantifier
✔ Ready for resolution
🔥 What You Probably Didn’t Understand
Most students get confused about:
❓ Why we remove ∀ ?
Because in clause form, all variables are assumed universally quantified.
❓ Why z became f(y)?
Because existential quantifiers are removed using Skolemization.