Notation
- ¬ not · ∧ and · ∨ or · ⇒ implies.
- Resolution (Robinson): to prove a goal, add its negation, convert everything to CNF, split into clauses, then resolve until the empty clause ⊥ appears.
- Chaining works on Horn rules (IF–THEN) + facts.
Part 1 — Resolution (Robinson's method)
Exercise 1
Chain + case split on disjunction
Given that the following premises are true:
1. u
2. v
3. u ⇒ p
4. v ⇒ q
5. (p ∧ q) ⇒ r
6. r ⇒ (s ∨ t)
7. s ⇒ w
8. t ⇒ w
Prove that w is true by Robinson's method.
Note: this mixes a chain
u, v → p, q → r with a case split on the disjunction s ∨ t.
Show your work
- Step 0 — Negate goal: add ¬w
- Step 1 — Convert all premises + negated goal to CNF
- Step 2 — List the clause set
- Step 3 — Resolution: resolve pairs until ⊥ (empty clause)
Step 0 (negate goal):
Step 1 (CNF):
Step 2 (clause set):
Step 3 (resolution chain → ⊥):
Exercise 2
Proof by cases on p ∨ q
Given that the following premises are true:
1. p ∨ q
2. p ⇒ (r ∧ s)
3. q ⇒ (r ∧ t)
4. (r ∧ s) ⇒ u
5. (r ∧ t) ⇒ u
6. u ⇒ v
(a) Prove that v is true by Robinson's method.
(b) Then prove u as well.
Hint: a proof by cases on
p ∨ q; note each conjunctive conclusion r ∧ s, r ∧ t splits into two clauses in CNF.
Show your work (for each proof)
- Step 0 — Negate goal
- Step 1 — Convert to CNF
- Step 2 — Clause set
- Step 3 — Resolution chain → ⊥
(a) Prove v:
Step 0–3:
(b) Prove u:
Step 0–3:
Part 2 — Forward & Backward Chaining
Exercise 3
Tet Holiday — Prove G ("visit Grandma")
Symbols:
| Symbol | Meaning | Symbol | Meaning | |
|---|---|---|---|---|
| T | Tet is coming | V | Visit new, beautiful places | |
| B | There is a bonus | M | Visit My Dinh | |
| F | Have fun | G | Visit Grandma | |
| P | Go out / play |
Rules (Horn):
R1: T ∧ B ⇒ F
R2: F ⇒ P
R3: P ⇒ V
R4: V ⇒ M
R5: M ⇒ G
Facts: T, B. Query: prove G.
Tasks
- Solve by forward chaining: list the firing order of the rules and the propositions derived at each step.
- Solve by backward chaining: draw the goal–subgoal decomposition tree.
- (Extension) Add rule R6: B ⇒ Shopping. What does forward chaining additionally derive? Does backward chaining (goal G) ever use R6? State your observation.
1. Forward chaining:
Firing order and derived propositions:
2. Backward chaining:
Goal–subgoal tree:
3. Extension (R6: B ⇒ Shopping):
Forward chaining additionally derives: Backward chaining uses R6? Observation:
Exercise 4
Driving in Rain — Prove Danger
Symbols:
- Rain = it is raining
- Wet = the road is wet
- Slippery = the road is slippery
- Driving = you are driving
- Danger = danger
Rules (Horn):
R1: Rain ⇒ Wet
R2: Wet ⇒ Slippery
R3: Slippery ∧ Driving ⇒ Danger
Facts: Rain, Driving. Query: prove Danger.
Tasks
Solve by forward chaining and by backward chaining; point out where the AND-rule (R3) is used.
Forward chaining:
Firing order and derived propositions:
Backward chaining:
Goal–subgoal tree (note where AND-rule R3 appears):
Total: 4 exercises — 2 parts following the slide sequence. Show all steps clearly to receive full marks.