Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished(~~(p /\ ~q) || ~~(p /\ ~q)) /\ (F || p) /\ T /\ T /\ (F || p) /\ ~~T /\ ~F /\ (~~(T /\ q) || ~r) /\ ~~~~(p /\ ~~~q) /\ ~~T /\ ~q /\ ~F /\ ~q
⇒ logic.propositional.idempor~~(p /\ ~q) /\ (F || p) /\ T /\ T /\ (F || p) /\ ~~T /\ ~F /\ (~~(T /\ q) || ~r) /\ ~~~~(p /\ ~~~q) /\ ~~T /\ ~q /\ ~F /\ ~q
⇒ logic.propositional.notnotp /\ ~q /\ (F || p) /\ T /\ T /\ (F || p) /\ ~~T /\ ~F /\ (~~(T /\ q) || ~r) /\ ~~~~(p /\ ~~~q) /\ ~~T /\ ~q /\ ~F /\ ~q