So I'm doing a problem in the book but this problem (where they ask me to use proof by resolution) seems unnecessary:
$p\iff r$
$r$
$\therefore p$
By definition of IFF, this seems true, but they ask me to prove by resolution? How do I go about it? If p IFF r is true, and r is true, by definition of If and Only If, doesn't that justify p being true?
We want to prove :
$((p \rightarrow r) \land (r \rightarrow p), r \vDash p$ ---(*).
Due to the equivalence between $a \rightarrow b$ with $\lnot a \lor b$, the above is equivalent to :
$[(\lnot p \lor r) \land (\lnot r \lor p) \land r] \vDash p$
and this in turn is equivalent to :
$\vDash [(\lnot p \lor r) \land (\lnot r \lor p) \land r ] \rightarrow p$.
We know that the a formula is valid iff its negation is unsatisfiable.
Thus, in order to prove (*), we have to show that :
$[(\lnot p \lor r) \land (\lnot r \lor p) \land r] \land \lnot p$
is unsatisfiable.
Thus, we have to apply Resolution to the set of clauses :
$\{ \lnot p \lor r, \lnot r \lor p, r, \lnot p \}$
and deriving the empty clause.
This shows that the set of clauses is unsatisfiable, and thus the argument is valid.
