Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(~T /\ r) || ~(~(q /\ T) /\ ~~~F /\ T /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T) /\ T /\ T /\ T) || F
⇒ logic.propositional.falsezeroor(~T /\ r) || ~(~(q /\ T) /\ ~~~F /\ T /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T) /\ T /\ T /\ T)
⇒ logic.propositional.idempand(~T /\ r) || ~(~(q /\ T) /\ ~~~F /\ T /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T) /\ T /\ T)
⇒ logic.propositional.idempand(~T /\ r) || ~(~(q /\ T) /\ ~~~F /\ T /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T) /\ T)
⇒ logic.propositional.nottrue(F /\ r) || ~(~(q /\ T) /\ ~~~F /\ T /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T) /\ T)
⇒ logic.propositional.falsezeroandF || ~(~(q /\ T) /\ ~~~F /\ T /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T) /\ T)
⇒ logic.propositional.falsezeroor~(~(q /\ T) /\ ~~~F /\ T /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T) /\ T)
⇒ logic.propositional.truezeroand~(~(q /\ T) /\ ~~~F /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T) /\ T)
⇒ logic.propositional.truezeroand~(~(q /\ T) /\ ~~~F /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T))
⇒ logic.propositional.notnot~(~(q /\ T) /\ ~F /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T))
⇒ logic.propositional.notfalse~(~(q /\ T) /\ T /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~(q /\ T) /\ ~(T /\ ~~F) /\ ~~~p /\ ~(q /\ T))
⇒ logic.propositional.notnot~(~(q /\ T) /\ ~(T /\ ~~F) /\ ~p /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~q /\ ~(T /\ ~~F) /\ ~p /\ ~(q /\ T))
⇒ logic.propositional.truezeroand~(~q /\ ~~~F /\ ~p /\ ~(q /\ T))
⇒ logic.propositional.notnot~(~q /\ ~F /\ ~p /\ ~(q /\ T))
⇒ logic.propositional.notfalse~(~q /\ T /\ ~p /\ ~(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