Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished((T /\ q) || ~r) /\ (~(~(~q /\ ~p) /\ ~q) -> (T /\ F))
⇒ logic.propositional.falsezeroand((T /\ q) || ~r) /\ (~(~(~q /\ ~p) /\ ~q) -> F)
⇒ logic.propositional.demorganand((T /\ q) || ~r) /\ ((~~(~q /\ ~p) || ~~q) -> F)
⇒ logic.propositional.notnot((T /\ q) || ~r) /\ (((~q /\ ~p) || ~~q) -> F)
⇒ logic.propositional.notnot((T /\ q) || ~r) /\ (((~q /\ ~p) || q) -> F)
⇒ logic.propositional.oroverand((T /\ q) || ~r) /\ (((~q || q) /\ (~p || q)) -> F)
⇒ logic.propositional.complor((T /\ q) || ~r) /\ ((T /\ (~p || q)) -> F)
⇒ logic.propositional.truezeroand((T /\ q) || ~r) /\ ((~p || q) -> F)
⇒ logic.propositional.defimpl((T /\ q) || ~r) /\ (~(~p || q) || F)
⇒ logic.propositional.demorganor((T /\ q) || ~r) /\ ((~~p /\ ~q) || F)
⇒ logic.propositional.falsezeroor((T /\ q) || ~r) /\ ~~p /\ ~q
⇒ logic.propositional.notnot((T /\ q) || ~r) /\ p /\ ~q