Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
Derivation
![](http://ideas.cs.uu.nl/images/external.png)
~q => p || (~(p || q) /\ ~p)
⇒ logic.propositional.oroverand~q => (p || ~(p || q)) /\ (p || ~p)
⇒ logic.propositional.complor~q => (p || ~(p || q)) /\ T
⇒ logic.propositional.demorganor~q => (p || (~p /\ ~q)) /\ T
⇒ logic.propositional.oroverand~q => (p || ~p) /\ (p || ~q) /\ T
⇒ logic.propositional.complor~q => T /\ (p || ~q) /\ T
⇒ logic.propositional.truezeroand~q => (p || ~q) /\ T
⇒ logic.propositional.truezeroand~q => p || ~q
⇒ introfalseleftF || ~q => p || ~q
⇒ introcompl(p /\ ~p) || ~q => p || ~q
⇒ logic.propositional.oroverand(p || ~q) /\ (~p || ~q) => p || ~q
⇒ conj-elimp || ~q => p || ~q