Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
All applications
Rule | commor.sort |
Location | [0,0,1] |
(p || (~p /\ ~q)) /\ ((~p /\ ~q) || q), ~p => ~q
ready: no
(p || (~p /\ ~q)) /\ (q || (~p /\ ~q)) /\ ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0] |
F || ((p || (~p /\ ~q)) /\ (q || (~p /\ ~q))), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,0] |
(F || p || (~p /\ ~q)) /\ (q || (~p /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,0,0] |
(F || p || (~p /\ ~q)) /\ (q || (~p /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,0,1] |
(p || F || (~p /\ ~q)) /\ (q || (~p /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,0,1,0] |
(p || ((F || ~p) /\ ~q)) /\ (q || (~p /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,0,1,0,0] |
(p || (~(F || p) /\ ~q)) /\ (q || (~p /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,0,1,1] |
(p || (~p /\ (F || ~q))) /\ (q || (~p /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,0,1,1,0] |
(p || (~p /\ ~(F || q))) /\ (q || (~p /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,1] |
(p || (~p /\ ~q)) /\ (F || q || (~p /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,1,0] |
(p || (~p /\ ~q)) /\ (F || q || (~p /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,1,1] |
(p || (~p /\ ~q)) /\ (q || F || (~p /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,1,1,0] |
(p || (~p /\ ~q)) /\ (q || ((F || ~p) /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,1,1,0,0] |
(p || (~p /\ ~q)) /\ (q || (~(F || p) /\ ~q)), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,1,1,1] |
(p || (~p /\ ~q)) /\ (q || (~p /\ (F || ~q))), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,0,1,1,1,0] |
(p || (~p /\ ~q)) /\ (q || (~p /\ ~(F || q))), ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,1] |
(p || (~p /\ ~q)) /\ (q || (~p /\ ~q)), F || ~p => ~q
ready: no
Rule | introfalseleft |
Location | [0,1,0] |
(p || (~p /\ ~q)) /\ (q || (~p /\ ~q)), ~(F || p) => ~q
ready: no
Rule | introfalseleft |
Location | [1] |
(p || (~p /\ ~q)) /\ (q || (~p /\ ~q)), ~p => F || ~q
ready: no
Rule | introfalseleft |
Location | [1,0] |
(p || (~p /\ ~q)) /\ (q || (~p /\ ~q)), ~p => ~(F || q)
ready: no
Rule | logic.propositional.andoveror |
Location | [0,0] |
((p || (~p /\ ~q)) /\ q) || ((p || (~p /\ ~q)) /\ ~p /\ ~q), ~p => ~q
ready: no
Rule | logic.propositional.andoveror |
Location | [0,0] |
(p /\ (q || (~p /\ ~q))) || (~p /\ ~q /\ (q || (~p /\ ~q))), ~p => ~q
ready: no
Rule | logic.propositional.oroverand |
Location | [0,0,0] |
(p || ~p) /\ (p || ~q) /\ (q || (~p /\ ~q)), ~p => ~q
ready: no
Rule | logic.propositional.oroverand |
Location | [0,0,1] |
(p || (~p /\ ~q)) /\ (q || ~p) /\ (q || ~q), ~p => ~q
ready: no