Can anyone help me with a solution?

Question

Write down the assumptions in a form of clauses and give a resolution proof that the proposition $$\Big((p \rightarrow q) \land ( q \rightarrow r) \land p \Big) \rightarrow r$$ is a tautology.

Answer 1

Well, you have $p$ in the antecedent, and you have $p\rightarrow q$, and together, by modus ponens, you get $q$. Now, $q$, with the implication $q\rightarrow r$ give you $r$, again, using modus ponens.

So the conjunction in the antecedent (i.e. the three conjuncts in the antecedent) imply $r$.

Can you now use this to complete your assignment? Remember, the main connective here is an implication. The only way it can be false is if the antecedent is true but the consequent is false. By using the above rules of inference, you are guaranteed that if the antecedent (and hence each of the conjuncts) is true, so is the conclusion. I.e, the implication cannot be false.

Alternatively, you can proceed as follows (but you supply the justification for each line):$$\begin{align}\Big((p \rightarrow q) \land ( q \rightarrow r) \land p \Big) \rightarrow r &\equiv \lnot \big((p\rightarrow q) \land (q\rightarrow r) \land p\big) \lor r\\ \\ &\equiv \lnot\big((\lnot p \lor q) \land (\lnot q \lor r) \land p\big) \lor r\\ \\ &\equiv (\lnot(\lnot p \lor q) \lor \lnot(\lnot q \lor r) \lor \lnot p)\lor r\\ \\ &\equiv (p \land \lnot q) \lor (q \land \lnot r)\lor \lnot p \lor r\\ \\ &\equiv [(\lnot p \lor p) \land (\lnot p \lor \lnot q)] \lor [(r\lor q) \land (r \lor \lnot r)] \\ \\ &\equiv \lnot p \lor \lnot q \lor r \lor q\\ \\ &\equiv T\end{align}$$

Answer 2

The negation of the goal has the following conjunctive normal form: $$ \lnot(((p \rightarrow q) \land ( q \rightarrow r) \land p) \rightarrow r) \equiv (\lnot p \lor q) \land (\lnot q \lor r) \land p \land \lnot r $$ I.e., you have four clauses: $$ \begin{array}{cl} A:& \{\lnot p, q\}\\ B:& \{\lnot q, r\}\\ C:& \{p\}\\ D:& \{\lnot r\} \end{array} $$ $A$, $B$ and $C$ give the "assumptions in clause form" that your question is asking for. The rest of the resolution proof goes like this: $$ \begin{array}{clr} E:& \{\lnot q\} & [B, D] \\ F:& \{\lnot p\} & [A, E] \\ G:& \{\mathsf{false}\} & [C, F] \end{array} $$ where the letters in square brackets tell you which earlier clauses to resolve to get the new clause. We have derived $\mathsf{false}$ from the negation of the goal by putting it into clause form and applying resolution inference steps. That constitutes a resolution proof of the goal.