I'm looking into rules of inference and in particular resolution, e.g.

$$((p ∨ q) ∧ (¬p ∨ r)) → (q ∨ r)$$

Now in the textbook I see the following example but I don't quite understand it

Show that the premises (p ∧ q) ∨ r and r → s imply the conclusion p ∨ s.
And here are the steps from the textbook to show this:

  1. Rewrite (p ∧ q) ∨ r as (p ∨ r) ∧ (q ∨ r)
  2. Rewrite r → s by the equivalent clause ¬r ∨ s
  3. Using the resolution we can conclude p ∨ s

Now I'm having a bit trouble understanding the above. To me the task is to show this:

$$((p ∧ q) ∨ r) ∧ (r → s) → p ∨ s$$

Now while I understand where first 2 steps come from, can't quite get my head around the 3rd one. After first 2 steps this is what we have (I think)

$$((p ∨ r) ∧ (q ∨ r)) ∧ (¬r ∨ s)$$

How it goes from here to conclude that

$$((p ∨ r) ∧ (q ∨ r)) ∧ (¬r ∨ s) → p ∨ s$$

is what I'm having hard time understanding.

I tried to use Commutativity, Associativity to go from

$$((p ∨ r) ∧ (q ∨ r)) ∧ (¬r ∨ s)$$


$$((r ∨ p) ∧ (¬r ∨ s)) ∧ (q ∨ r)$$

Here I see that the first part is a Resolution: $$((r ∨ p) ∧ (¬r ∨ s)) → (p ∨ s)$$

but can't understand what about: $$∧ (q ∨ r)$$


It's extra information we don't need. Since it's connect with an AND, we can discard it if necessary. Using conjunction elimination, we know from: $$ ((r ∨ p) ∧ (¬r ∨ s)) ∧ (q ∨ r) $$

we can infer that: $$ (r ∨ p) ∧ (¬r ∨ s) $$

and so by resolution, we conclude that $p \lor s$, as desired.

  • $\begingroup$ Thank you! Didn't know about conjunction elimination, makes perfect sense now. $\endgroup$
    – Michael
    Oct 16 '17 at 7:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.