Exercise logic.propositional.consequence

Description
Prove that formula is a logical consequence of a set of formulas

Feedback

• onefirst
• allfirsts (2)
• allapplications
• derivation
• microsteps

Environment

initial=TList [TVar "q"]

Path 1

path	[0, 0, 4, 0, 0, 3, 0, 0, 0, 0, 1, 5, 1, 0, 2, 0, 0, 0, 0, 4, 0, 0, 0, 2, 0, 2, 1, 0, 2, 0, 0, 0, 4]
steps	33
major rules	3
active labels	consequence

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, check, enter simplify, enter orrules, logic.propositional.complor, exit orrules, exit simplify, navigator.up, check, navigator.down, navigator.right, check, navigator.down, navigator.right, check, enter simplify, enter orrules, logic.propositional.complor