Logical consequence/resolution dilemma

Question

Show with resolution that logical consequence $p \Rightarrow (\neg q \rightarrow p)$ holds.

I have been stuck with this problem for a while now, can someone give me starting point?

Answer 1

Showing that $\lnot q \to p$ (the thesis) is a logical consequence of $p$ (the hypothesis), amounts to show that the formula $p \land \lnot (\lnot q \to p)$ (obtained as the conjunction of the hypotheses and of the negation of the thesis) is unsatisfiable.

To prove that such a formula is unsatisfiable, we first have to transform it in an equivalent conjunction of literals (conjunctive normal form). Now,

$$\lnot( \lnot q \to p) \equiv \lnot (\lnot \lnot q \lor p) \equiv \lnot (q \lor p) \equiv \lnot q \land \lnot p $$ and so $$p \land \lnot (\lnot q \to p) \equiv p \land \lnot q \land \lnot p$$ which is a conjunctive normal form. Such a formula is unsatisfiable if and only if the set of clauses:

$$\tag{1} \{p, \lnot q, \lnot p\}$$

is unsatisfiable. According to the resolution method, a set of clauses is unsatisfiable if and only if it is possible to derive the empty clause by applying repeatedly the resolution rule to any pair of clauses of that set. Let us take the clauses $p$ and $\lnot p$ from the set $(1)$ and let us apply the resolution rule to them: we get the empty clause

$$\dfrac{p \qquad \lnot p}{\square} $$

Therefore, the set $(1)$ is unsatisfiable, which is equivalent to say that $\lnot q \to p$ is a logical consequence of $p$.