Use the rules of inference to show that if $\forall x(P(x) \lor Q(x))$ and $\forall x(\lnot P(x) \land Q(x) \to R(x))$ are true. then $\forall x (\lnot R(x) \to P(x))$ is true where the domains of all quantifiers is the same. 
I'm getting caught up on step 7 below. 


*

*$\forall x (P(x) \lor Q(x)$ (Premise)

*$P(c) \lor Q(c)$ (Universal Instantiation from 1)

*$\forall x (\lnot P(x) \land Q(x) \to R(x)$ (Premise)

*$\lnot P(c) \land Q(c) \to R(c)$ (Universal Instantiation from 2)

*$\lnot(\lnot P(c) \land Q(c)) \lor R(c)$ (Conditional Logical Equivalence)

*$P(c) \lor \lnot Q(c) \lor R(c)$ (DeMorgan's Law)

*$\lnot P(c) \lor R(c)$ (Resolution 2 and 6)


^^^ How can 7 be the results of the resolution of 2 and 6? When I try and work it out I'm left with the following:
2-a. $Q(c) \lor P(c)$ (Commutative Law)
6-a. $\lnot Q(c) \lor P(c) \lor R(c)$ (Commutative Law)
7-a. $P(c) \lor P(c) \lor R(c)$ (Resolution 2 and 6)
--- Continuing on can I apply the Idempotent law to 7-a?


*$R(c) \lor P(c)$ (Idempotent and Commutative Laws)

*$\lnot R(c) \to P(c)$ (Conditional Logical Equivalence)

*$\forall x (\lnot R(x) \to P(x))$ Universal Generalization
QED.
 A: Your reasoning in 2-a through 10 is correct. 
Line 7 does not follow from 2 and 6. To see this, you can use a model theoretic approach to show that $\neg P(c) \vee R(c)$ is not a logical implication of $P(c) \vee Q(c)$ and $P(c) \vee \neg Q(c) \vee R(c)$.
For example, let
\begin{equation}
P(c) = T\\
Q(c) = T\\
R(c) = F.
\end{equation}
Then we have
\begin{equation}
(P(c) \vee Q(c)) = T\\
(P(c) \vee \neg Q(c) \vee R(c)) = T\\
\neg P(c) \vee R(c) = F.
\end{equation}
Thus, the conditional $[(P(c) \vee Q(c)) \wedge (P(c) \vee \neg Q(c) \vee R(c))] \rightarrow (\neg P(c) \vee R(c))$ is false in this model, which means that you cannot infer $\neg P(c) \vee R(c)$ from the other two propositions in a proof theoretic setting. Of course, this all presupposes that the logical system you are using is sound :).
A: You are correct, $\lnot P(c)\lor R(c)$ is not the result of resolution of those lines.   Fortunately it is also not what you want to obtain from the resolution.
$\{\{p, q\},\{p,\lnot q,r\}\}$ resolves to $\{\{p,r\}\}$ ...which is also $\{\{p,\lnot\lnot r\}\}$
Thusly, line 7 should be $P(c)\lor R(c)$, which is equivalent to $P(c)\lor\lnot\lnot R(c)$, and thus $\lnot R(c)\to P(c)$, as you require.

  
*
  
*$\forall x~(P(x) \lor Q(x))$ (Premise I)
  
*$\forall x~((\lnot P(x) \land Q(x)) \to R(x)$ (Premise II)
  
*$\quad P(c) \lor Q(c)$ (Universal Instantiation from 1 to arbitrary $c$)
  
*$\quad (\lnot P(c) \land Q(c)) \to R(c)$ (Universal Instantiation from 2)
  
*$\quad \lnot(\lnot P(c) \land Q(c)) \lor R(c)$ (Conditional Logical Equivalence)
  
*$\quad P(c) \lor \lnot Q(c) \lor R(c)$ (DeMorgan's Law)
  
*$\quad P(c) \lor R(c)$ (Resolution 3 and 6)
  
*$\quad \lnot R(c)\to P(c)$ (Conditional Logical Equivalence from 7)
  
*$\forall x~(\lnot R(x)\to P(x))$ (Universal Generalisation, from 8 and arbitrary $c$)
  

