Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
All applications
Rule | absorpand-subset |
Location | [1,0,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | command.sort |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => T /\ (p || ~p) /\ ((p /\ q /\ p) || ~(p /\ q)) /\ (q || ~p)
ready: no
Rule | command.sort |
Location | [1,0,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ p /\ q) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | command.sort |
Location | [1,0,0,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ p /\ q) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | command.sort |
Location | [1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (p || ~p) /\ (q || ~p)
ready: no
Rule | command.sort |
Location | [1,1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (p || ~p) /\ (q || ~p)
ready: no
Rule | commor.sort |
Location | [1,1,1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (~p || q) /\ (p || ~p)
ready: no
Rule | compland.sort |
Location | [1,0,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ p /\ q) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [0,0] |
![](http://ideas.cs.uu.nl/images/external.png)
F || q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => F || (((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p))
ready: no
Rule | introfalseleft |
Location | [1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => (F || (p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,0,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => (F || (p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,0,0,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => (((F || p) /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,0,0,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ (F || (q /\ p))) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,0,0,1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ (F || q) /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,0,0,1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ (F || p)) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,0,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || F || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,0,1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(F || (p /\ q))) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,0,1,0,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~((F || p) /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,0,1,0,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ (F || q))) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ (F || (T /\ (q || ~p) /\ (p || ~p)))
ready: no
Rule | introfalseleft |
Location | [1,1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ (F || T) /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (F || ((q || ~p) /\ (p || ~p)))
ready: no
Rule | introfalseleft |
Location | [1,1,1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (F || q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,1,1,0,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (F || q || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,1,1,0,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || F || ~p) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,1,1,0,1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~(F || p)) /\ (p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,1,1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (F || p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,1,1,1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (F || p || ~p)
ready: no
Rule | introfalseleft |
Location | [1,1,1,1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || F || ~p)
ready: no
Rule | introfalseleft |
Location | [1,1,1,1,1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~(F || p))
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => (((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ p) || (((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ ~p)
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((((p /\ q /\ p) || ~(p /\ q)) /\ T /\ q) || (((p /\ q /\ p) || ~(p /\ q)) /\ T /\ ~p)) /\ (p || ~p)
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ ((T /\ (q || ~p) /\ p) || (T /\ (q || ~p) /\ ~p))
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (((q || ~p) /\ p) || ((q || ~p) /\ ~p))
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ ((T /\ q) || (T /\ ~p)) /\ (p || ~p)
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => (p /\ q /\ p /\ T /\ (q || ~p) /\ (p || ~p)) || (~(p /\ q) /\ T /\ (q || ~p) /\ (p || ~p))
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p /\ T) || (~(p /\ q) /\ T)) /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p /\ T /\ (q || ~p)) || (~(p /\ q) /\ T /\ (q || ~p))) /\ (p || ~p)
ready: no
Rule | logic.propositional.andoveror |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ ((q /\ (p || ~p)) || (~p /\ (p || ~p)))
ready: no
Rule | logic.propositional.andoveror |
Location | [1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ ((T /\ (q || ~p) /\ p) || (T /\ (q || ~p) /\ ~p))
ready: no
Rule | logic.propositional.andoveror |
Location | [1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ ((T /\ q) || (T /\ ~p)) /\ (p || ~p)
ready: no
Rule | logic.propositional.andoveror |
Location | [1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (((q || ~p) /\ p) || ((q || ~p) /\ ~p))
ready: no
Rule | logic.propositional.andoveror |
Location | [1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ ((q /\ (p || ~p)) || (~p /\ (p || ~p)))
ready: no
Rule | logic.propositional.andoveror |
Location | [1,1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (((q || ~p) /\ p) || ((q || ~p) /\ ~p))
ready: no
Rule | logic.propositional.andoveror |
Location | [1,1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ ((q /\ (p || ~p)) || (~p /\ (p || ~p)))
ready: no
Rule | logic.propositional.complor |
Location | [1,1,1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ T
ready: no
Rule | logic.propositional.demorganand |
Location | [1,0,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~p || ~q) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | logic.propositional.genoroverand |
Location | [1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => (p || ~(p /\ q)) /\ (q || ~(p /\ q)) /\ (p || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | logic.propositional.oroverand |
Location | [1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => (p || ~(p /\ q)) /\ ((q /\ p) || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | logic.propositional.oroverand |
Location | [1,0] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q) || ~(p /\ q)) /\ (p || ~(p /\ q)) /\ T /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | logic.propositional.truezeroand |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | logic.propositional.truezeroand |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | logic.propositional.truezeroand |
Location | [1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ (q || ~p) /\ (p || ~p)
ready: no
Rule | logic.propositional.truezeroand |
Location | [1,1] |
![](http://ideas.cs.uu.nl/images/external.png)
q => ((p /\ q /\ p) || ~(p /\ q)) /\ (q || ~p) /\ (p || ~p)
ready: no