Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished(~~~q /\ ((~((p -> q) || F) /\ ~~~q /\ ~((p -> q) || F)) || F)) -> p
⇒ logic.propositional.falsezeroor(~~~q /\ ~((p -> q) || F) /\ ~~~q /\ ~((p -> q) || F)) -> p
⇒ logic.propositional.falsezeroor(~~~q /\ ~(p -> q) /\ ~~~q /\ ~((p -> q) || F)) -> p
⇒ logic.propositional.falsezeroor(~~~q /\ ~(p -> q) /\ ~~~q /\ ~(p -> q)) -> p
⇒ logic.propositional.notnot(~~~q /\ ~(p -> q) /\ ~q /\ ~(p -> q)) -> p
⇒ logic.propositional.defimpl(~~~q /\ ~(~p || q) /\ ~q /\ ~(p -> q)) -> p
⇒ logic.propositional.demorganor(~~~q /\ ~~p /\ ~q /\ ~q /\ ~(p -> q)) -> p
⇒ logic.propositional.idempand(~~~q /\ ~~p /\ ~q /\ ~(p -> q)) -> p
⇒ logic.propositional.notnot(~~~q /\ p /\ ~q /\ ~(p -> q)) -> p
⇒ logic.propositional.defimpl(~~~q /\ p /\ ~q /\ ~(~p || q)) -> p
⇒ logic.propositional.demorganor(~~~q /\ p /\ ~q /\ ~~p /\ ~q) -> p
⇒ logic.propositional.notnot(~~~q /\ p /\ ~q /\ p /\ ~q) -> p
⇒ logic.propositional.idempand(~~~q /\ p /\ ~q) -> p