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