Disjunctive normal form of (¬(p → q) → (q ∧ ¬r))

Question

I learning how to convert to disjunctive normal forms, I have the following,

(¬(p → q) → (q ∧ ¬r))

I understand any p→q can be represented as (¬p)∨q, therefore if I image the above as just that I can break each section down, resulting in:

1. p → q == (¬p)∨ q, therefore (¬(p → q) == ¬((¬p) ∨ q
2. ¬((¬p) ∨ q → (q ∧ ¬r)) == ¬(¬((¬p)∨q)) ∨ (q ∧ ¬r )

Therefore the disjunctive form is:
¬(¬((¬p)∨q)) ∨ (q ∧ ¬r )

The truth table for this seems to match, is this correct? I have a feeling I have left a step out, maybe repetition of the NOT could be fixed?

Answer 1

$\neg(p\Rightarrow q) \Leftrightarrow \neg(\neg p\vee q)$

and so

$\neg(p\Rightarrow q) \Rightarrow (q\wedge \neg r)$

is equivalent to

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

is equivalent to

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

is equivalent to

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

By absorption $a\vee (a\wedge b) \Leftrightarrow a$, it is equivalent to

$\neg p\vee q$.

Answer 2

Using SymPy:

>>> from sympy import * 
>>> p, q, r = symbols('p q r')
>>> phi = Not(p >> q) >> (q & Not(r))

Converting to DNF and simplifying:

>>> to_dnf(phi, simplify=False)
q | ~p | (q & ~r)
>>> to_dnf(phi, simplify=True)
q | ~p

Hence, we have the DNF formulas

$$q \vee \left(q \wedge \neg r\right) \vee \neg p \equiv q \vee \neg p$$