Exercise logic.propositional.proof.top
Description
Prove two propositions equivalent (with top-level decomposition)
Examples
easy (7)
~(p /\ q) || s || ~r == (p /\ q) -> (r -> s)
p || ~(p || ~q) == p || q
p /\ q == ~(p -> ~q)
q /\ p == p /\ (q || q)
~(~p /\ ~(q || r)) == p || q || r
~(p /\ (q || r)) == ~p || (~q /\ ~r)
p <-> q == ~p <-> ~q
medium (14)
~((p -> q) -> (p /\ q)) == (p -> q) /\ (~p || ~q)
~((p <-> q) -> (p || (p <-> q))) == F
(p /\ q) -> p == T
p -> q == ~q -> ~p, p -> s == ~s -> ~p
p || (~p /\ q) == p || q
(p -> q) || ~p == (p -> q) || q
(p -> q) || (q -> p) == T
(p -> ~q) -> q == (s || (s -> (q || p))) /\ q
(p -> q) -> ~p == p -> (q -> ~p)
(~q /\ p) -> p == (~q <-> q) -> p
p <-> (p /\ q) == p -> q
p <-> (p -> q) == p /\ q
(p -> q) /\ (r -> q) == (p || r) -> q
p /\ (q || s) == (q /\ ~s /\ p) || (p /\ s)
difficult (10)
(p /\ ~q) || (q /\ ~p) == (p || q) /\ ~(p /\ q)
(p /\ q /\ r) || (~p /\ q) == (~p /\ q /\ ~r) || (q /\ r)
p <-> q == (p -> q) /\ (q -> p)
(q -> (~p -> q)) -> p == ~p -> (q /\ p /\ q /\ q)
p -> (q -> r) == (p -> q) -> (p -> r)
~((p -> q) -> ~(q -> p)) == p <-> q
p <-> (q <-> p) == q
(p -> q) <-> (p -> r) == (p -> (q /\ r)) || ~(p -> (q || r))
p || (q /\ r) == (p /\ ~q) || (p /\ ~r) || (q /\ r)
(p /\ q) || (~q /\ r) == (p /\ r) || (p /\ q /\ ~r) || (~p /\ ~q /\ r)