Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
((~(~q /\ ~~~p /\ ~q /\ ~~~p) || (~~q /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p))) /\ (~~(r /\ T /\ T) || (~~q /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p)))) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.absorpor(~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ (~~(r /\ T /\ T) || (~~q /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p)))) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.idempand(~(~q /\ ~~~p) /\ (~~(r /\ T /\ T) || (~~q /\ ~(~q /\ ~~~p /\ ~q /\ ~~~p)))) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.idempand(~(~q /\ ~~~p) /\ (~~(r /\ T /\ T) || (~~q /\ ~(~q /\ ~~~p)))) || (~(~q /\ ~~~p /\ ~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.idempand(~(~q /\ ~~~p) /\ (~~(r /\ T /\ T) || (~~q /\ ~(~q /\ ~~~p)))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.notnot(~(~q /\ ~p) /\ (~~(r /\ T /\ T) || (~~q /\ ~(~q /\ ~~~p)))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.notnot(~(~q /\ ~p) /\ ((r /\ T /\ T) || (~~q /\ ~(~q /\ ~~~p)))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.idempand(~(~q /\ ~p) /\ ((r /\ T) || (~~q /\ ~(~q /\ ~~~p)))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.notnot(~(~q /\ ~p) /\ ((r /\ T) || (q /\ ~(~q /\ ~~~p)))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.notnot(~(~q /\ ~p) /\ ((r /\ T) || (q /\ ~(~q /\ ~p)))) || (~(~q /\ ~~~p) /\ ~~~~p)
⇒ logic.propositional.notnot(~(~q /\ ~p) /\ ((r /\ T) || (q /\ ~(~q /\ ~p)))) || (~(~q /\ ~p) /\ ~~~~p)
⇒ logic.propositional.notnot(~(~q /\ ~p) /\ ((r /\ T) || (q /\ ~(~q /\ ~p)))) || (~(~q /\ ~p) /\ ~~p)
⇒ logic.propositional.notnot(~(~q /\ ~p) /\ ((r /\ T) || (q /\ ~(~q /\ ~p)))) || (~(~q /\ ~p) /\ p)
⇒ logic.propositional.demorganand(~(~q /\ ~p) /\ ((r /\ T) || (q /\ ~(~q /\ ~p)))) || ((~~q || ~~p) /\ p)
⇒ logic.propositional.notnot(~(~q /\ ~p) /\ ((r /\ T) || (q /\ ~(~q /\ ~p)))) || ((q || ~~p) /\ p)
⇒ logic.propositional.notnot(~(~q /\ ~p) /\ ((r /\ T) || (q /\ ~(~q /\ ~p)))) || ((q || p) /\ p)
⇒ logic.propositional.absorpand(~(~q /\ ~p) /\ ((r /\ T) || (q /\ ~(~q /\ ~p)))) || p
⇒ logic.propositional.truezeroand(~(~q /\ ~p) /\ (r || (q /\ ~(~q /\ ~p)))) || p
⇒ logic.propositional.demorganand((~~q || ~~p) /\ (r || (q /\ ~(~q /\ ~p)))) || p
⇒ logic.propositional.notnot((q || ~~p) /\ (r || (q /\ ~(~q /\ ~p)))) || p
⇒ logic.propositional.notnot((q || p) /\ (r || (q /\ ~(~q /\ ~p)))) || p
⇒ logic.propositional.demorganand((q || p) /\ (r || (q /\ (~~q || ~~p)))) || p
⇒ logic.propositional.notnot((q || p) /\ (r || (q /\ (q || ~~p)))) || p
⇒ logic.propositional.absorpand((q || p) /\ (r || q)) || p
⇒ logic.propositional.andoveror((q || p) /\ r) || ((q || p) /\ q) || p
⇒ logic.propositional.absorpand((q || p) /\ r) || q || p
⇒ logic.propositional.absorporq || p