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