Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished~~~~(((~r /\ ~~(p /\ ~q)) || (q /\ ~~(p /\ ~q))) /\ ~~(p /\ ~q))
⇒ logic.propositional.notnot~~(((~r /\ ~~(p /\ ~q)) || (q /\ ~~(p /\ ~q))) /\ ~~(p /\ ~q))
⇒ logic.propositional.notnot~~(((~r /\ p /\ ~q) || (q /\ ~~(p /\ ~q))) /\ ~~(p /\ ~q))
⇒ logic.propositional.notnot~~(((~r /\ p /\ ~q) || (q /\ p /\ ~q)) /\ ~~(p /\ ~q))
⇒ logic.propositional.notnot~~(((~r /\ p /\ ~q) || (q /\ p /\ ~q)) /\ p /\ ~q)
⇒ logic.propositional.gendemorganand~(~((~r /\ p /\ ~q) || (q /\ p /\ ~q)) || ~p || ~~q)
⇒ logic.propositional.demorganor~((~(~r /\ p /\ ~q) /\ ~(q /\ p /\ ~q)) || ~p || ~~q)
⇒ logic.propositional.gendemorganand~(((~~r || ~p || ~~q) /\ ~(q /\ p /\ ~q)) || ~p || ~~q)
⇒ logic.propositional.notnot~(((r || ~p || ~~q) /\ ~(q /\ p /\ ~q)) || ~p || ~~q)
⇒ logic.propositional.notnot~(((r || ~p || q) /\ ~(q /\ p /\ ~q)) || ~p || ~~q)
⇒ logic.propositional.gendemorganand~(((r || ~p || q) /\ (~q || ~p || ~~q)) || ~p || ~~q)
⇒ logic.propositional.notnot~(((r || ~p || q) /\ (~q || ~p || q)) || ~p || ~~q)
⇒ logic.propositional.genandoveror~(((r || ~p || q) /\ ~q) || ((r || ~p || q) /\ ~p) || ((r || ~p || q) /\ q) || ~p || ~~q)
⇒ logic.propositional.absorpand~(((r || ~p || q) /\ ~q) || ((r || ~p || q) /\ ~p) || q || ~p || ~~q)
⇒ logic.propositional.genandoveror~((r /\ ~q) || (~p /\ ~q) || (q /\ ~q) || ((r || ~p || q) /\ ~p) || q || ~p || ~~q)
⇒ logic.propositional.compland~((r /\ ~q) || (~p /\ ~q) || F || ((r || ~p || q) /\ ~p) || q || ~p || ~~q)
⇒ logic.propositional.falsezeroor~((r /\ ~q) || (~p /\ ~q) || ((r || ~p || q) /\ ~p) || q || ~p || ~~q)
⇒ logic.propositional.genandoveror~((r /\ ~q) || (~p /\ ~q) || (r /\ ~p) || (~p /\ ~p) || (q /\ ~p) || q || ~p || ~~q)
⇒ logic.propositional.absorpor~((r /\ ~q) || (~p /\ ~q) || (r /\ ~p) || (~p /\ ~p) || q || ~p || ~~q)
⇒ logic.propositional.idempand~((r /\ ~q) || (~p /\ ~q) || (r /\ ~p) || ~p || q || ~p || ~~q)
⇒ logic.propositional.absorpor~((r /\ ~q) || (~p /\ ~q) || ~p || q || ~p || ~~q)
⇒ logic.propositional.absorpor~((r /\ ~q) || ~p || q || ~p || ~~q)
⇒ logic.propositional.notnot~((r /\ ~q) || ~p || q || ~p || q)
⇒ logic.propositional.idempor~((r /\ ~q) || ~p || q)