Proof by Resolution in Propositional Logic
Proof by Resolution is one of the most important theorem-proving techniques in Artificial Intelligence. It is used to determine whether a conclusion logically follows from a set of propositions.
It is particularly important because resolution can be implemented efficiently by computers, making it useful for automated theorem proving.
1. What is Resolution?
Definition
Resolution is an inference rule used in propositional logic to derive a new clause from two clauses containing complementary literals.
For example:\[ P\lor Q \]
and\[ \neg P\lor R \]
can be resolved to produce:\[ Q\lor R \]
The complementary literals are:\[ P \quad \text{and} \quad \neg P \]
So:\[ \boxed{(P\lor Q),(\neg P\lor R)\Rightarrow(Q\lor R)} \]
2. Basic Idea of Proof by Resolution
Resolution normally uses proof by contradiction.
Suppose we want to prove:\[ KB\models Q \]
Instead of directly proving Q, we:
- Take the knowledge base.
- Negate the conclusion.
- Add the negated conclusion to the knowledge base.
- Convert everything into Conjunctive Normal Form (CNF).
- Apply the resolution rule repeatedly.
- Try to derive an empty clause.
- If an empty clause is obtained, a contradiction has been found.
- Therefore, the original conclusion is proved.
Basic formula
\[ \boxed{KB\models Q} \]
is proved by showing:\[ \boxed{KB\land\neg Q\Rightarrow\bot} \]
where:\[ \bot = \text{Contradiction} \]
3. Why Do We Negate the Conclusion?
This is the central idea students should understand.
Suppose we want to prove:
The road is wet.
Instead of directly proving:\[ Wet \]
we assume:\[ \neg Wet \]
If the existing knowledge says that the road must be wet, then we get a contradiction.
Therefore:\[ \neg Wet \]
must be false.
Hence:\[ Wet \]
must be true.
Diagram
Want to prove Q
|
↓
Assume ¬Q
|
↓
Combine with Knowledge
|
↓
Apply Resolution
|
↓
Contradiction
|
↓
Therefore
Q
4. Important Terms
Before learning the algorithm, understand these terms.
Literal
A literal is either a proposition or its negation.
Examples:\[ P \]\[ \neg P \]
Both are literals.
Clause
A clause is a disjunction (OR) of literals.
Examples:\[ P\lor Q \]\[ \neg P\lor R \]\[ P\lor\neg Q\lor R \]
Complementary Literals
Two literals are complementary if one is the negation of the other.
Examples:\[ P,\neg P \]\[ Q,\neg Q \]
These are the literals that resolution eliminates.
5. The Resolution Rule
The basic resolution rule is:\[ \boxed{ (P\lor Q),(\neg P\lor R) \Rightarrow (Q\lor R) } \]
Let’s understand it.
First clause:\[ P\lor Q \]
Second clause:\[ \neg P\lor R \]
Since:\[ P \]
and:\[ \neg P \]
are complementary, they are eliminated.
The remaining literals are:\[ Q\lor R \]
Therefore:\[ \boxed{Q\lor R} \]
is the resolvent.
6. What is a Resolvent?
The new clause produced by applying the resolution rule is called the resolvent.
Example:\[ P\lor Q \]
and:\[ \neg P\lor R \]
produce:\[ Q\lor R \]
Therefore:\[ Q\lor R \]
is the resolvent.
7. Simple Example of Resolution
Given:\[ P\lor Q \]\[ \neg P \]
We can resolve them.
Write the second clause as:\[ \neg P\lor False \]
The complementary pair is:\[ P,\neg P \]
Eliminate them.
Remaining:\[ Q \]
Therefore:\[ \boxed{Q} \]
8. Proof by Resolution — Complete Example
Let’s prove a simple statement.
Knowledge
- If it rains, the road is wet.
- It is raining.
Prove:
The road is wet.
Step 1: Define propositions
Let:\[ P = \text{It is raining} \]\[ Q = \text{Road is wet} \]
Knowledge base:\[ P \]\[ P\rightarrow Q \]
Goal:\[ Q \]
9. Step 2: Negate the Goal
The goal is:\[ Q \]
Negate it:\[ \neg Q \]
Now we have:\[ P \]\[ P\rightarrow Q \]\[ \neg Q \]
10. Step 3: Convert Implication to OR
Resolution works with clauses, so convert:\[ P\rightarrow Q \]
using:\[ P\rightarrow Q\equiv\neg P\lor Q \]
Therefore the clauses are:\[ P \]\[ \neg P\lor Q \]\[ \neg Q \]
11. Step 4: Apply Resolution
First resolve:\[ P \]
with:\[ \neg P\lor Q \]
Complementary literals:\[ P,\neg P \]
Remaining:\[ Q \]
So we derive:\[ Q \]
Now resolve:\[ Q \]
with:\[ \neg Q \]
We get:\[ \boxed{\square} \]
The symbol:\[ \square \]
represents the empty clause, meaning contradiction.
Therefore:\[ \boxed{Q} \]
is proved.
12. Complete Proof Diagram
Knowledge Base:
P
P → Q
+
Negated Goal:
¬Q
|
↓
Convert P → Q
|
↓
¬P ∨ Q
|
↓
Resolve P with ¬P ∨ Q
|
↓
Q
|
↓
Resolve Q with ¬Q
|
↓
□ ← Empty Clause
|
↓
Contradiction
|
↓
Therefore Q is TRUEThis is the basic pattern you should remember.
13. Why is the Empty Clause Important?
The empty clause is normally represented as:\[ \boxed{\square} \]
or:\[ \boxed{\bot} \]
It means falsehood or contradiction.
When proof by resolution produces the empty clause, it means:
Our assumption that the conclusion was false leads to a contradiction.
Therefore the original conclusion must be true.
14. General Resolution Procedure
The general algorithm is:
Step 1
Represent the knowledge base in propositional logic.
Step 2
Identify the conclusion/query.
Step 3
Negate the conclusion.
Step 4
Combine:\[ KB\land\neg Goal \]
Step 5
Convert the resulting expressions into Conjunctive Normal Form (CNF).
Step 6
Apply the resolution rule.
Step 7
Generate new clauses.
Step 8
Continue resolving clauses.
Step 9
If:\[ \square \]
is obtained, the goal is proved.
Step 10
If no new clauses can be generated and no empty clause is obtained, the goal cannot be proved from the given knowledge base using this resolution procedure.
15. Resolution Algorithm
We can represent it as:
START
|
↓
Knowledge Base + Goal
|
↓
Negate Goal
|
↓
Convert to CNF
|
↓
Create Clauses
|
↓
Select Two Clauses
|
↓
Find Complementary Literals
|
↓
Apply Resolution
|
↓
Generate Resolvent
|
├───────────────┐
↓ ↓
Empty Clause? No
| |
Yes ↓
| Continue Resolution
↓ |
PROVED └──────→ Repeat16. Why CNF is Required?
Resolution works on clauses, and clauses are normally represented as disjunctions of literals.
The complete expression is represented as a conjunction of clauses.
This is called:
Conjunctive Normal Form (CNF)
General CNF
\[ (A\lor B)\land(C\lor D)\land(E\lor F) \]
Each bracket is a clause.
17. Example of CNF
Consider:\[ (P\rightarrow Q)\land R \]
First remove implication:\[ (\neg P\lor Q)\land R \]
This is already in CNF.
Clauses are:\[ (\neg P\lor Q) \]
and:\[ R \]
18. Steps for Converting to CNF
This is very important for resolution problems.
Usually follow these steps:
Step 1 — Eliminate biconditionals
\[ P\leftrightarrow Q \]
becomes:\[ (P\rightarrow Q)\land(Q\rightarrow P) \]
Step 2 — Eliminate implications
Use:\[ P\rightarrow Q\equiv\neg P\lor Q \]
Step 3 — Move NOT inward
Use De Morgan’s Laws:\[ \neg(P\land Q) \equiv \neg P\lor\neg Q \]\[ \neg(P\lor Q) \equiv \neg P\land\neg Q \]
Step 4 — Distribute OR over AND
Use:\[ P\lor(Q\land R) \]
becomes:\[ (P\lor Q)\land(P\lor R) \]
Step 5 — Obtain CNF
The final expression should be:\[ Clause_1\land Clause_2\land Clause_3… \]
19. CNF Example
Convert:\[ P\rightarrow(Q\land R) \]
to CNF.
Step 1: Remove implication
\[ \neg P\lor(Q\land R) \]
Step 2: Distribute OR
\[ (\neg P\lor Q)\land(\neg P\lor R) \]
Therefore:\[ \boxed{(\neg P\lor Q)\land(\neg P\lor R)} \]
is the CNF.
20. More Complete Resolution Example
Let’s consider:
Given
- If it rains, the road is wet.
- If the road is wet, traffic slows.
- It is raining.
Prove:
Traffic slows.
Step 1: Define propositions
\[ P = Rain \]\[ Q = WetRoad \]\[ R = SlowTraffic \]
Knowledge:\[ P \]\[ P\rightarrow Q \]\[ Q\rightarrow R \]
Goal:\[ R \]
Step 2: Negate goal
\[ \neg R \]
Step 3: Convert implications
\[ P\rightarrow Q \]
becomes:\[ \neg P\lor Q \]
and:\[ Q\rightarrow R \]
becomes:\[ \neg Q\lor R \]
So clauses are:\[ P \]\[ \neg P\lor Q \]\[ \neg Q\lor R \]\[ \neg R \]
Step 4: Resolve
Resolve:\[ P \]
with:\[ \neg P\lor Q \]
Result:\[ Q \]
Now resolve:\[ Q \]
with:\[ \neg Q\lor R \]
Result:\[ R \]
Finally resolve:\[ R \]
with:\[ \neg R \]
Result:\[ \boxed{\square} \]
Therefore:\[ \boxed{R} \]
is proved.
21. Resolution Refutation
The method described above is also called:
Resolution Refutation
Why?
Because we refute the negation of the goal.
The process is:\[ KB\land\neg Goal \]
If this produces:\[ \bot \]
then:\[ KB\models Goal \]
Remember:
Negate Goal
↓
Assume Goal is false
↓
Find contradiction
↓
Therefore Goal is true22. Resolution vs Modus Ponens
Both are inference methods, but they work differently.
| Modus Ponens | Resolution |
|---|---|
| Direct inference rule | Refutation-based theorem proving |
| \(P, P→Q \Rightarrow Q\) | Works with clauses |
| Does not require negating goal | Usually negates goal |
| Simple reasoning | Automated theorem proving |
| Works directly with implications | Requires CNF/clause form |
23. Resolution vs Truth Table
| Truth Table | Resolution |
|---|---|
| Model-based | Proof-based |
| Examines truth assignments | Applies inference rules |
| Can require \(2^n\) rows | Avoids explicit enumeration of all models |
| Simple for small problems | Better suited to automated theorem proving |
| Tests entailment | Constructs a refutation/proof |
24. Important Properties of Resolution
1. Soundness
Resolution is sound.
If it derives a conclusion, the conclusion is logically valid.
2. Completeness
For propositional logic, resolution is refutation-complete.
This means:
If a set of clauses is unsatisfiable, resolution can derive the empty clause, given appropriate systematic application of the rule.
This is one of the reasons resolution is important in AI.
25. Resolution in AI
Resolution has applications in:
- automated theorem proving
- knowledge representation
- expert systems
- logical reasoning
- automated planning
- verification
- symbolic AI
The general architecture is:
Knowledge Base
|
↓
Logical Clauses
|
↓
Query / Goal
|
↓
Negate Goal
|
↓
Resolution Engine
|
↓
┌───────────┴───────────┐
↓ ↓
Empty Clause No Empty Clause
↓ ↓
Proved Not Proved
26. Common Mistakes in Resolution
Mistake 1: Not negating the goal
If the goal is:\[ Q \]
you must generally add:\[ \neg Q \]
for resolution refutation.
Mistake 2: Not converting implications
Do not directly resolve:\[ P\rightarrow Q \]
Instead convert:\[ P\rightarrow Q \equiv \neg P\lor Q \]
Mistake 3: Resolving non-complementary literals
You can resolve:\[ P \]
with:\[ \neg P \]
but not:\[ P \]
with:\[ Q \]
because they are not complementary.
Mistake 4: Forgetting the empty clause
The objective is generally:\[ \boxed{\square} \]
A contradiction proves the original goal.
27. Easy Numerical/Logical Example for Students
Given:\[ P\lor Q \]\[ \neg P\lor R \]
Apply resolution.
Identify complementary literals
\[ P,\neg P \]
Remove them.
Remaining:\[ Q\lor R \]
Therefore:\[ \boxed{Q\lor R} \]
is the resolvent.
28. Another Example
Given:\[ P\lor Q \]\[ \neg Q\lor R \]
Resolve on Q.
Remove:\[ Q,\neg Q \]
Remaining:\[ P\lor R \]
Therefore:\[ \boxed{P\lor R} \]
29. Resolution Example with Three Clauses
Given:\[ P\lor Q \]\[ \neg Q\lor R \]\[ \neg R \]
First resolution
Resolve:\[ P\lor Q \]
and:\[ \neg Q\lor R \]
Result:\[ P\lor R \]
Second resolution
Resolve:\[ P\lor R \]
with:\[ \neg R \]
Result:\[ P \]
Therefore:\[ \boxed{P} \]
has been derived.
This illustrates how resolution can progressively simplify the knowledge base.
30. Key Formula to Remember
The most important resolution rule is:\[ \boxed{ \frac{P\lor Q,\quad\neg P\lor R} {Q\lor R} } \]
And the most important proof strategy is:\[ \boxed{ KB\models Goal \quad\text{if}\quad KB\land\neg Goal \Rightarrow \square } \]
31. Exam-Oriented Answer
Definition
Proof by Resolution is a refutation-based theorem-proving technique in propositional logic. It proves a goal by adding the negation of the goal to the knowledge base, converting the resulting expressions into Conjunctive Normal Form, and repeatedly applying the resolution rule. If the empty clause is derived, a contradiction is obtained and the original goal is proved.
Main steps
- Represent the knowledge base.
- Identify the goal.
- Negate the goal.
- Convert all expressions into CNF.
- Extract clauses.
- Find complementary literals.
- Apply resolution.
- Generate new clauses.
- Continue until:
- empty clause is obtained → proved
- no new useful clauses can be generated → not proved
32. One Complete Flow to Memorize
KNOWLEDGE BASE
+
NEGATED GOAL
|
↓
Convert to
CNF
|
↓
CLAUSES
|
↓
Find Complementary
Literals
|
↓
RESOLUTION
|
↓
New Clause
|
┌──────┴──────┐
↓ ↓
Empty Clause? No
| |
Yes ↓
| Continue
↓ Resolution
CONTRADICTION
|
↓
ORIGINAL GOAL
PROVED
Quick memory trick: N-C-R-C
N → Negate the goal
C → Convert to CNF
R → Resolve clauses
C → Contradiction / empty clause
Negate → CNF → Resolve → Contradiction = Proof by Resolution.
The next closely connected topic in your syllabus is Horn Clauses and Definite Clauses, where we see how restricted forms of propositional logic make inference more efficient, particularly through forward and backward chaining.