Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
q => ((p /\ q /\ p) || ~(p /\ q)) /\ (p || ~p) /\ (q || ~p) /\ T
ready: no
Feedback
Environment
initial=TList [TVar "q"]
Path 1
| path | [0, 0, 4, 0, 0, 3, 0, 0, 0, 0, 1, 5, 1, 0, 2, 0, 2, 1, 0, 2, 0, 0, 0, 4] |
| steps | 24 |
| major rules | 2 |
| active labels | - consequence
- simplify
- orrules
|
enter consequence,
initial,
navigator.down,
navigator.down,
enter cnf,
exit cnf,
navigator.up,
navigator.up,
navigator.downlast,
enter cnf,
check,
enter distror,
logic.propositional.genoroverand,
exit distror,
check,
navigator.down,
navigator.right,
check,
navigator.down,
navigator.right,
check,
enter simplify,
enter orrules,
logic.propositional.complor