Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished~q /\ ~F /\ ~~T /\ ~(~T || ~((T /\ q) || ~r) || ~(T /\ p /\ ~q) || ~(~~(p /\ ~q) /\ p) || ~(~~~~(p /\ ~q) /\ T) || ~~F)
⇒ logic.propositional.notnot~q /\ ~F /\ ~~T /\ ~(~T || ~((T /\ q) || ~r) || ~(T /\ p /\ ~q) || ~(p /\ ~q /\ p) || ~(~~~~(p /\ ~q) /\ T) || ~~F)
⇒ logic.propositional.gendemorganand~q /\ ~F /\ ~~T /\ ~(~T || ~((T /\ q) || ~r) || ~(T /\ p /\ ~q) || ~p || ~~q || ~p || ~(~~~~(p /\ ~q) /\ T) || ~~F)
⇒ logic.propositional.notnot~q /\ ~F /\ ~~T /\ ~(~T || ~((T /\ q) || ~r) || ~(T /\ p /\ ~q) || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T) || ~~F)
⇒ logic.propositional.notnot~q /\ ~F /\ ~~T /\ ~(~T || ~((T /\ q) || ~r) || ~(T /\ p /\ ~q) || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T) || F)
⇒ logic.propositional.falsezeroor~q /\ ~F /\ ~~T /\ ~(~T || ~((T /\ q) || ~r) || ~(T /\ p /\ ~q) || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T))
⇒ logic.propositional.nottrue~q /\ ~F /\ ~~T /\ ~(F || ~((T /\ q) || ~r) || ~(T /\ p /\ ~q) || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T))
⇒ logic.propositional.falsezeroor~q /\ ~F /\ ~~T /\ ~(~((T /\ q) || ~r) || ~(T /\ p /\ ~q) || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T))
⇒ logic.propositional.truezeroand~q /\ ~F /\ ~~T /\ ~(~(q || ~r) || ~(T /\ p /\ ~q) || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T))
⇒ logic.propositional.demorganor~q /\ ~F /\ ~~T /\ ~((~q /\ ~~r) || ~(T /\ p /\ ~q) || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T))
⇒ logic.propositional.notnot~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~(T /\ p /\ ~q) || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T))
⇒ logic.propositional.truezeroand~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~(p /\ ~q) || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T))
⇒ logic.propositional.demorganand~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~p || ~~q || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T))
⇒ logic.propositional.notnot~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~p || q || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T))
⇒ logic.propositional.idempor~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~p || q || ~p || ~(~~~~(p /\ ~q) /\ T))
⇒ logic.propositional.truezeroand~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~p || q || ~p || ~~~~~(p /\ ~q))
⇒ logic.propositional.notnot~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~p || q || ~p || ~~~(p /\ ~q))
⇒ logic.propositional.notnot~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~p || q || ~p || ~(p /\ ~q))
⇒ logic.propositional.demorganand~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~p || q || ~p || ~p || ~~q)
⇒ logic.propositional.idempor~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~p || q || ~p || ~~q)
⇒ logic.propositional.notnot~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~p || q || ~p || q)
⇒ logic.propositional.idempor~q /\ ~F /\ ~~T /\ ~((~q /\ r) || ~p || q)