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