proving-modus-ponens-resolution

Modus Ponens,

$(p\wedge (p\to q))\to q$

Let’s tryna prove this using contradiction by checking satisfiability using resolution method.

$\neg ((p\wedge (p\to q))\to q)$

It can be solved more as shown below.

$(p\wedge (p\to q))\wedge \neg q$, using $\neg (A\to B)\equiv A\wedge \neg B$

Simplifying it further,

$p\wedge (\neg p\vee q)\wedge \neg q$

Converting it into clausal form,

$$\begin{gathered} \text{displaylines}\{p\}-(1) \\ \{\neg p,q\}-(2) \\ \{\neg q\}-(3) \end{gathered}$$

Using $(1)$ and $(2)$,

$$\begin{gathered} \text{displaylines}\{q\}...(1),(2)-(3) \\ \{\neg q\}-(4) \end{gathered}$$

Further down,

$$\text{displaylines}\{\}...(3),(4)$$

We get empty set which depicts negation of modus ponens is unsatisfiable. Hence proved that Modus Ponens is a tautology.