Exercise

Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

(T /\ ~(T /\ ~(q /\ T) /\ ~~~F /\ T /\ ~~~F /\ ~(q /\ T) /\ ~~~p /\ T /\ T) /\ T /\ ~(T /\ ~(q /\ T) /\ ~~~F /\ T /\ ~~~F /\ ~(q /\ T) /\ ~~~p /\ T /\ T)) || (~T /\ r)

⇒ logic.propositional.idempand

(T /\ ~(T /\ ~(q /\ T) /\ ~~~F /\ T /\ ~~~F /\ ~(q /\ T) /\ ~~~p /\ T /\ T)) || (~T /\ r)

⇒ logic.propositional.truezeroand

~(T /\ ~(q /\ T) /\ ~~~F /\ T /\ ~~~F /\ ~(q /\ T) /\ ~~~p /\ T /\ T) || (~T /\ r)

⇒ logic.propositional.idempand

~(T /\ ~(q /\ T) /\ ~~~F /\ T /\ ~~~F /\ ~(q /\ T) /\ ~~~p /\ T) || (~T /\ r)

⇒ logic.propositional.truezeroand

~(~(q /\ T) /\ ~~~F /\ T /\ ~~~F /\ ~(q /\ T) /\ ~~~p /\ T) || (~T /\ r)

⇒ logic.propositional.truezeroand

~(~(q /\ T) /\ ~~~F /\ ~~~F /\ ~(q /\ T) /\ ~~~p /\ T) || (~T /\ r)

⇒ logic.propositional.idempand

~(~(q /\ T) /\ ~~~F /\ ~(q /\ T) /\ ~~~p /\ T) || (~T /\ r)

⇒ logic.propositional.truezeroand

~(~(q /\ T) /\ ~~~F /\ ~(q /\ T) /\ ~~~p) || (~T /\ r)

⇒ logic.propositional.notnot

~(~(q /\ T) /\ ~F /\ ~(q /\ T) /\ ~~~p) || (~T /\ r)

⇒ logic.propositional.notfalse

~(~(q /\ T) /\ T /\ ~(q /\ T) /\ ~~~p) || (~T /\ r)

⇒ logic.propositional.truezeroand

~(~(q /\ T) /\ ~(q /\ T) /\ ~~~p) || (~T /\ r)

⇒ logic.propositional.idempand

~(~(q /\ T) /\ ~~~p) || (~T /\ r)

⇒ logic.propositional.notnot

~(~(q /\ T) /\ ~p) || (~T /\ r)

⇒ logic.propositional.truezeroand

~(~q /\ ~p) || (~T /\ r)

⇒ logic.propositional.demorganand

~~q || ~~p || (~T /\ r)

⇒ logic.propositional.notnot

q || ~~p || (~T /\ r)

⇒ logic.propositional.notnot

q || p || (~T /\ r)