Exercise

Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.absorpor

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.notfalse

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

⇒ logic.propositional.notfalse

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

⇒ logic.propositional.notfalse

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.notfalse

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

⇒ logic.propositional.absorpor

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroand

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

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.notfalse

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.notfalse

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.notnot

p /\ ~q /\ ~r /\ p /\ ~q