Introduction to Logic
Tools
for
Thought
 

Exercise 14.5 - Resolution

Given the premises ∀x.(p(x) ⇒ q(x)) and ∀x.(q(x) ⇒ r(x)), use Resolution to prove the conclusion ∀x.(p(x) ⇒ r(x)).

Robinson
Undo Copy Paste Load Save Help
Objects: a, b, c
Functions: f, g
Goal  Incomplete

















1 {~p(X),q(X)} Premise 2 {~q(X),r(X)} Premise 3 {p(a)} Negated Goal 4 {~r(a)} Negated Goal 5 {q(a)} Resolution 3 1 6 {r(a)} Resolution 5 2 7 {} Resolution 6 4