The problem is as follows: Given the premise ∀x(P (x) ∨ Q(x)) and ∀x((¬P (x) ∧ Q(x)) → R(x)) is true, use the rules of inference to show that ∀x(¬R(x) → P(x)) is also true. (The domains of all quantifiers are the same)
Now, I have a vague idea of how to do this and have the following work:
(1) ∀x(P (x) ∨ Q(x))
Premise # 1
(2) ∀x((¬P (x) ∧ Q(x)) → R(x))
Premise # 2
(3) P(a) ∨ Q(a)
Universal Instantiation on (1)
(4) ¬R(a)
(5) ¬(¬P(a) ∧ Q(a))
Universal Modus Tollens
(6) P(a) ∨¬Q(a)
Simplification of (5)
(7) P(a) ∨ P(a)
Resolution of (2) and (6)
(8) P(a)
Simplification of (7)
(9) ¬R(x) → P(x)
Assuming (4), it implies (8)
(10) ∀x(¬R(x) → P(x))
Universal Generalization of (9)
Now my main problem is how to deal with the Universal Modus Tollens in (4) and (5). Particularly how can I just say ¬R(a)? And then how do I get from ¬R(a) and P(a) to ¬R(x) → P(x)? What do I have to do to make this whole thing flow logically and correctly? Am I missing something?
I believe you'll need to use universal instantiation on $(2)$. As a universally quantified premise, you can instantiate with $\,a\,$, as you did with premise $(1)$, (since the domain of all the quantifiers is the same) then use modus tollens when you need it, applied to the instantiated statement and using the assumption $\lnot R$.
Also, as currently numbered, I think you need to justify resolution for line $(7)$ by citing $(3)$ and $(6)$ (I'm assuming you're referring to resolution to $\,P(a)\,$ given the statements $\,\left[P(a) \lor Q(a)\right]\;$ and $\left[P(a) \lor \lnot Q(a)\right].$
The key here is that you want your steps (currently numbered) $4 - 8$ indented (to designate a "sub-proof", where $(4)$ is stated as an "assumption", then $5$ follows from $(4)$ and the (soon to be) instantiated step resulting from $(2)$.
Line $(9)$ should still be a statement about the constant $a$, not $x$ as written, citing sub-proof, $(4 - 8)$ (by assuming (4), we obtain (8)), i.e. $(4)\rightarrow (8)$ given subproof $4-8$.
From $9$ to $10$ then, you are correct, as is your justification of universal generalization.