Exercise logic.propositional.consequence

Description
Prove that formula is a logical consequence of a set of formulas

Derivation

Final term is not finished

q => (p || ((~p || ~q) /\ ~p)) /\ ((q /\ p) || ((~p || ~q) /\ ~p))

⇒ logic.propositional.absorpand, initial=TList [TVar "q"]

q => (p || ((~p || ~q) /\ ~p)) /\ ((q /\ p) || ~p)

⇒ logic.propositional.oroverand

q => (p || ((~p || ~q) /\ ~p)) /\ (q || ~p) /\ (p || ~p)

⇒ logic.propositional.complor

q => (p || ((~p || ~q) /\ ~p)) /\ (q || ~p) /\ T

⇒ logic.propositional.truezeroand

q => (p || ((~p || ~q) /\ ~p)) /\ (q || ~p)

⇒ absorpand-subset

q => (p || ~p) /\ (q || ~p)