Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

(p || q) /\ ~(T /\ ~(r <-> p))

⇒ logic.propositional.truezeroand

(p || q) /\ ~~(r <-> p)

⇒ logic.propositional.defequiv

(p || q) /\ ~~((r /\ p) || (~r /\ ~p))

⇒ logic.propositional.demorganor

(p || q) /\ ~(~(r /\ p) /\ ~(~r /\ ~p))

⇒ logic.propositional.demorganand

(p || q) /\ ~(~(r /\ p) /\ (~~r || ~~p))

⇒ logic.propositional.notnot

(p || q) /\ ~(~(r /\ p) /\ (r || ~~p))

⇒ logic.propositional.notnot

(p || q) /\ ~(~(r /\ p) /\ (r || p))

⇒ logic.propositional.demorganand

(p || q) /\ ~((~r || ~p) /\ (r || p))

⇒ logic.propositional.andoveror

(p || q) /\ ~(((~r || ~p) /\ r) || ((~r || ~p) /\ p))

⇒ logic.propositional.andoveror

(p || q) /\ ~((~r /\ r) || (~p /\ r) || ((~r || ~p) /\ p))

⇒ logic.propositional.andoveror

(p || q) /\ ~((~r /\ r) || (~p /\ r) || (~r /\ p) || (~p /\ p))

⇒ logic.propositional.compland

(p || q) /\ ~(F || (~p /\ r) || (~r /\ p) || (~p /\ p))

⇒ logic.propositional.compland

(p || q) /\ ~(F || (~p /\ r) || (~r /\ p) || F)

⇒ logic.propositional.falsezeroor

(p || q) /\ ~((~p /\ r) || (~r /\ p) || F)

⇒ logic.propositional.falsezeroor

(p || q) /\ ~((~p /\ r) || (~r /\ p))