Exercise logic.propositional.consequence
Description
Prove that formula is a logical consequence of a set of formulas
Rules for logic.propositional.consequence
| Rule name | Args | Used | Siblings | Rewrite rule |
| absorpand-subset | 0 | yes | ||
| assump-false | 0 | yes | ||
| command-subset | 0 | yes | ||
| command.sort | 0 | yes | ||
| commor.sort | 0 | yes | ||
| compland.sort | 0 | yes | logic.propositional.commutativity | |
| complor.sort | 0 | yes | logic.propositional.commutativity | |
| conj-elim | 0 | yes | ||
| conj-intro | 0 | yes | ||
| fakeabsorption | 0 | yes | ||
| fakeabsorptionnot | 0 | yes | ||
| introcompl | 0 | yes | ||
| introfalseleft | 0 | yes | p ⇒ F ∨ p | |
| logic.propositional.absorpand | 0 | yes | logic.propositional.absorption | p ∧ (p ∨ q) ⇒ p p ∧ (q ∨ p) ⇒ p (p ∨ q) ∧ p ⇒ p (q ∨ p) ∧ p ⇒ p |
| logic.propositional.absorpor | 0 | yes | logic.propositional.absorption | p ∨ (p ∧ q) ⇒ p p ∨ (q ∧ p) ⇒ p (p ∧ q) ∨ p ⇒ p (q ∧ p) ∨ p ⇒ p |
| logic.propositional.andoveror | 0 | yes | logic.propositional.distribution | p ∧ (q ∨ r) ⇒ (p ∧ q) ∨ (p ∧ r) (p ∨ q) ∧ r ⇒ (p ∧ r) ∨ (q ∧ r) |
| logic.propositional.compland | 0 | yes | logic.propositional.falsecomplement | p ∧ (¬p) ⇒ F (¬p) ∧ p ⇒ F |
| logic.propositional.complor | 0 | yes | logic.propositional.truecomplement | p ∨ (¬p) ⇒ T (¬p) ∨ p ⇒ T |
| logic.propositional.defequiv | 0 | yes | logic.propositional.equivalence | p ↔ q ⇒ (p ∧ q) ∨ ((¬p) ∧ (¬q)) |
| logic.propositional.defimpl | 0 | yes | logic.propositional.implication | p → q ⇒ (¬p) ∨ q |
| logic.propositional.demorganand | 0 | yes | logic.propositional.demorgan | ¬(p ∧ q) ⇒ (¬p) ∨ (¬q) |
| logic.propositional.demorganor | 0 | yes | logic.propositional.demorgan | ¬(p ∨ q) ⇒ (¬p) ∧ (¬q) |
| logic.propositional.falsezeroand | 0 | yes | logic.propositional.falseconjunction | F ∧ p ⇒ F p ∧ F ⇒ F |
| logic.propositional.falsezeroor | 0 | yes | logic.propositional.falsedisjunction | F ∨ p ⇒ p p ∨ F ⇒ p |
| logic.propositional.gendemorganand | 0 | yes | logic.propositional.demorgan | |
| logic.propositional.gendemorganor | 0 | yes | logic.propositional.demorgan | |
| logic.propositional.genoroverand | 0 | yes | logic.propositional.distribution | |
| logic.propositional.idempand | 0 | yes | logic.propositional.idempotency | p ∧ p ⇒ p |
| logic.propositional.idempor | 0 | yes | logic.propositional.idempotency | p ∨ p ⇒ p |
| logic.propositional.notfalse | 0 | yes | logic.propositional.group-notfalse | ¬F ⇒ T |
| logic.propositional.notnot | 0 | yes | logic.propositional.doublenegation | ¬(¬p) ⇒ p |
| logic.propositional.nottrue | 0 | yes | logic.propositional.group-nottrue | ¬T ⇒ F |
| logic.propositional.oroverand | 0 | yes | logic.propositional.distribution | p ∨ (q ∧ r) ⇒ (p ∨ q) ∧ (p ∨ r) (p ∧ q) ∨ r ⇒ (p ∨ r) ∧ (q ∨ r) |
| logic.propositional.truezeroand | 0 | yes | logic.propositional.trueconjunction | T ∧ p ⇒ p p ∧ T ⇒ p |
| logic.propositional.truezeroor | 0 | yes | logic.propositional.truedisjunction | T ∨ p ⇒ T p ∨ T ⇒ T |
| top-is-and.com | 0 | yes |
Buggy rules for logic.propositional.consequence
| Rule name | Args | Used | Siblings | Rewrite rule |