Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(~~F /\ r) || ~(~(q /\ T) /\ T /\ ~~~F /\ T /\ T /\ ~~~p /\ ~(T /\ ~~F) /\ T /\ ~(q /\ T)) || F
⇒ logic.propositional.falsezeroor(~~F /\ r) || ~(~(q /\ T) /\ T /\ ~~~F /\ T /\ T /\ ~~~p /\ ~(T /\ ~~F) /\ T /\ ~(q /\ T))
⇒ logic.propositional.idempand(~~F /\ r) || ~(~(q /\ T) /\ T /\ ~~~F /\ T /\ ~~~p /\ ~(T /\ ~~F) /\ T /\ ~(q /\ T))
⇒ logic.propositional.notnot(F /\ r) || ~(~(q /\ T) /\ T /\ ~~~F /\ T /\ ~~~p /\ ~(T /\ ~~F) /\ T /\ ~(q /\ T))
⇒ logic.propositional.falsezeroandF || ~(~(q /\ T) /\ T /\ ~~~F /\ T /\ ~~~p /\ ~(T /\ ~~F) /\ T /\ ~(q /\ T))
⇒ logic.propositional.falsezeroor~(~(q /\ T) /\ T /\ ~~~F /\ T /\ ~~~p /\ ~(T /\ ~~F) /\ T /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~(q /\ T) /\ ~~~F /\ T /\ ~~~p /\ ~(T /\ ~~F) /\ T /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~(q /\ T) /\ ~~~F /\ ~~~p /\ ~(T /\ ~~F) /\ T /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~(q /\ T) /\ ~~~F /\ ~~~p /\ ~(T /\ ~~F) /\ ~(q /\ T))
⇒ logic.propositional.notnot~(~(q /\ T) /\ ~F /\ ~~~p /\ ~(T /\ ~~F) /\ ~(q /\ T))
⇒ logic.propositional.notfalse~(~(q /\ T) /\ T /\ ~~~p /\ ~(T /\ ~~F) /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~(q /\ T) /\ ~~~p /\ ~(T /\ ~~F) /\ ~(q /\ T))
⇒ logic.propositional.notnot~(~(q /\ T) /\ ~p /\ ~(T /\ ~~F) /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~q /\ ~p /\ ~(T /\ ~~F) /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~q /\ ~p /\ ~~~F /\ ~(q /\ T))
⇒ logic.propositional.notnot~(~q /\ ~p /\ ~F /\ ~(q /\ T))
⇒ logic.propositional.notfalse~(~q /\ ~p /\ T /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~q /\ ~p /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~q /\ ~p /\ ~q)
⇒ logic.propositional.gendemorganand~~q || ~~p || ~~q
⇒ logic.propositional.notnotq || ~~p || ~~q
⇒ logic.propositional.notnotq || p || ~~q
⇒ logic.propositional.notnotq || p || q