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