CIS 125

14– Resolution Proof

For problems 1-4, use methods of resolution proof to determine whether each argument/proof is valid.

Hints: For problem 4, the logical and operator is present when two symbols are together in much the same way that implied multiplication works. Thus, xy can be thought of as (x^ y). Additionally, operators can be distributed, so that x v (y ^ z) is equivalent to (x v y) ^ (x v z). Similarly, x ^ (y v z) is equivalent to (x ^ y) v (x ^ z)

For problems 4 and 5, replace the and operators with equivalent expressions that use or and and. Hint: a b is equivalent to (~a v b).

Remember that Resolution depends on the rule: if p v q and ~p v r are both true, then q v r is true.

Additional hint (as though it will help you…): all of the proofs below are valid.

1. ~p v q v r

~q

~r

------------

~p

2. ~p v r

~r v q

p

------------

q

3. p q

p v q

------------

q

(Hard)

4. ~p v t

~q v s

~r v st

p v q v r v u

------------

s v t v u