Rules of inference proofs

I have the following:

Premise: {$p \lor q, q\rightarrow r,p \land s \rightarrow t, \lnot r, \lnot q \rightarrow u \land s$}, conclusion: $t$

I'm having a real hard understanding how to prove the above using rules of inference. I can't seem to see the broader picture of how to use these rules to prove anything. Here's my attempt.

1. $q \rightarrow r$ Premise

2. $\lnot r$ Premise

3. $\lnot q$ Modus Tollens using (2) and (1)

4. $p \lor q$ Premise

5. $q \lor r$ Resolution using (1) and (4)

and this is the point I get stuck. I have two more premises but can't see where or how they would resolve anywhere. Any hints?

$(1) + (4)$ do not imply $q\lor r$, so undo line $(5)$ We do have that $(3) + (4)$ imply $p$. If $p \lor q$, and $\lnot q$, then $p$. Perhaps this can be line $(5)$.

Suggestion for the next step $(6)$: from $(3),$ along with the premise $\lnot q \rightarrow (u \land s)$, it follows by modus ponens that $u \land s$.

(7) Now, extract $s$ from $u \land s$.

(8) Then introduce the conjunction: $p \land s$. $p$ is from your new (5th) step, and $s$ from step (7).

Now we can use the premise $p\land s \implies t$ and $p \land s$ from step (8) to conclude by modus ponens that $t$, as desired

Key point: If you haven't used a premise, think of how it might help get you from what you have to what you need to establish. Always keep the goal or target proposition in your mind.

• Gotcha! Thanks for the great explanation. – Dimitri Oct 3 '13 at 23:16
• @Amzoti - you totally right on that! Thanks! – Namaste Oct 4 '13 at 0:03

Here is something that does not directly use inference rules, so it is formally not what you want, but it would definitely guide my intuition about which inference rules to apply in which order.

Let's start from our goal: \begin{align} & t \\ \leftarrow & \;\;\;\;\;\text{"use $\;p \land s \to t\;$ -- the only thing we know about $\;t\;$"} \\ & p \land s \\ \end{align} Now there is only one other thing we know about $\;p\;$, viz. $\;p \lor q\;$, so if we want $\;p\;$ as the conclusion we need to rewrite it as $\;\lnot q \to p\;$. Similarly, the only other thing we know about $\;s\;$ is $\;\lnot q \to u \land s\;$, so if we want $\;s\;$ as the conclusion we need to split this into $\;\lnot q \to u\;$ and $\;\lnot q \to s\;$.

We can now continue our calculation: \begin{align} & p \land s \\ \leftarrow & \;\;\;\;\;\text{"use $\;\lnot q \to p\;$ and $\;\lnot q \to s\;$, see above"} \\ & \lnot q \\ \leftarrow & \;\;\;\;\;\text{"use $\;q \to r\;$ in reverse -- the only thing left we know about $\;q\;$"} \\ & \lnot r \\ \leftrightarrow & \;\;\;\;\;\text{"use $\;\lnot r\;$ "} \\ & \text{true} \\ \end{align}

This completes the 'proof'.