Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
(~p || q) /\ p => q
ready: no
Feedback
Environment
initial=TList [TCon logic1.implies [TVar "p",TCon logic1.implies [TVar "p",TVar "q"]],TVar "p"]
Path 1
| path | [0, 0, 0, 3, 0, 0, 2, 0, 0, 3, 0, 0, 0, 2, 0, 0, 3, 1, 2, 0, 0, 0, 0, 2, 0, 0, 0, 0, 2] |
| steps | 29 |
| major rules | 4 |
| active labels | - consequence
- cnf
- simplify
- orrules
|
enter consequence,
initial,
conj-intro,
navigator.down,
navigator.down,
enter cnf,
check,
navigator.down,
check,
enter eliminateimplequiv,
logic.propositional.defimpl,
exit eliminateimplequiv,
navigator.up,
check,
navigator.down,
check,
enter eliminateimplequiv,
navigator.down,
navigator.right,
logic.propositional.defimpl,
navigator.up,
exit eliminateimplequiv,
navigator.up,
check,
navigator.down,
check,
enter simplify,
enter orrules,
logic.propositional.idempor