Proof that the formula $((p\to q)\land (q\to r)\land p)\to r$ is a tautology

Question

Write down the assumptions in a form of clauses and give a resolution proof that the formula is a tautology.

$((p\to q)\land (q\to r)\land p)\to r$

I got information that i need to use here Resolution calculus...Someone can help me?

Answer 1

In order to apply Resolution we consider that :

$\varphi \rightarrow \psi$ is a tautology iff its negation : $\varphi \land \lnot \psi$ is unsatisfiable.

Thus we consider the formula :

(*) $ \ ((p → q)∧(q → r)∧p) \land \lnot r$

and we apply the resolution technique to show that the new formula is unsatisfiable.

First, we transform into an equivalent sentence in conjunctive normal form :

$(\lnot p \lor q)∧(\lnot q \lor r) ∧ p \land \lnot r$

and then we build the set of clauses :

$\{ \lnot p \lor q \}$

$\{ \lnot q \lor r \}$

$\{ p \}$

$\{ \lnot r \}$.

Now we apply the resolution rule, trying to derive the empty clause : $\square$.

Using first and third we derive : $\{ q \}$; using it with second we derive : $\{ r \}$.

Finally, with $\{ r \}$ and fourth : $\{ \lnot r \}$, we derive the empty clause : $\square$.

Thus the formula (*) is unsatisfiable, and so the original formula is a tautology.