Exercise logic.propositional.cnf
Description
Proposition to CNF
Rules for logic.propositional.cnf
| Rule name | Args | Used | Siblings | Rewrite rule |
| andoveror.inv | 0 | no | logic.propositional.distribution | (p ∧ q) ∨ (p ∧ r) ⇒ p ∧ (q ∨ r) (p ∧ r) ∨ (q ∧ r) ⇒ (p ∨ q) ∧ r |
| compland.sort | 0 | yes | logic.propositional.commutativity | |
| complor.sort | 0 | yes | logic.propositional.commutativity | |
| defequiv.inv | 0 | no | logic.propositional.equivalence | (p ∧ q) ∨ ((¬p) ∧ (¬q)) ⇒ p ↔ q |
| defimpl.inv | 0 | no | logic.propositional.implication | (¬p) ∨ q ⇒ p → q |
| falsezeroor.inv | 0 | no | logic.propositional.falsedisjunction | p ⇒ F ∨ p p ⇒ p ∨ F |
| idempand.inv | 0 | no | logic.propositional.idempotency | p ⇒ p ∧ p |
| idempor.inv | 0 | no | logic.propositional.idempotency | p ⇒ p ∨ 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.assocand | 0 | no | logic.propositional.associativity | (p ∧ q) ∧ r ⇒ p ∧ (q ∧ r) |
| logic.propositional.assocor | 0 | no | logic.propositional.associativity | (p ∨ q) ∨ r ⇒ p ∨ (q ∨ r) |
| logic.propositional.command | 0 | no | logic.propositional.commutativity | p ∧ q ⇒ q ∧ p |
| logic.propositional.commor | 0 | no | logic.propositional.commutativity | p ∨ q ⇒ q ∨ p |
| 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.genandoveror | 0 | no | logic.propositional.distribution | |
| 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.invandoveror | 0 | no | logic.propositional.distribution | |
| logic.propositional.invdemorganand | 0 | no | logic.propositional.demorgan | |
| logic.propositional.invdemorganor | 0 | no | logic.propositional.demorgan | |
| logic.propositional.invoroverand | 0 | no | logic.propositional.distribution | |
| 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 |
| notfalse.inv | 0 | no | logic.propositional.group-notfalse | T ⇒ ¬F |
| notnot.inv | 0 | no | logic.propositional.doublenegation | p ⇒ ¬(¬p) |
| nottrue.inv | 0 | no | logic.propositional.group-nottrue | F ⇒ ¬T |
| oroverand.inv | 0 | no | logic.propositional.distribution | (p ∨ q) ∧ (p ∨ r) ⇒ p ∨ (q ∧ r) (p ∨ r) ∧ (q ∨ r) ⇒ (p ∧ q) ∨ r |
| truezeroand.inv | 0 | no | logic.propositional.trueconjunction | p ⇒ T ∧ p p ⇒ p ∧ T |
Buggy rules for logic.propositional.cnf
| Rule name | Args | Used | Siblings | Rewrite rule |
| logic.propositional.buggy.absor | 0 | no | (p ∨ q) ∨ ((p ∧ q) ∧ r) ⇏ p ∨ q (p ∧ q) ∨ ((p ∨ q) ∧ r) ⇏ p ∧ q (p ∨ q) ∧ ((p ∧ q) ∨ r) ⇏ p ∨ q (p ∧ q) ∧ ((p ∨ q) ∨ r) ⇏ p ∧ q | |
| logic.propositional.buggy.andcompl | 0 | no | p ∧ (¬p) ⇏ T (¬p) ∧ p ⇏ T p ∧ (¬p) ⇏ p (¬p) ∧ p ⇏ p | |
| logic.propositional.buggy.andcompl.inv | 0 | no | ||
| logic.propositional.buggy.andsame | 0 | no | p ∧ p ⇏ T | |
| logic.propositional.buggy.assimp | 0 | no | p → (q → r) ⇏ (p → q) → r (p → q) → r ⇏ p → (q → r) | |
| logic.propositional.buggy.assoc | 0 | no | p ∨ (q ∧ r) ⇏ (p ∨ q) ∧ r (p ∨ q) ∧ r ⇏ p ∨ (q ∧ r) (p ∧ q) ∨ r ⇏ p ∧ (q ∨ r) p ∧ (q ∨ r) ⇏ (p ∧ q) ∨ r | |
| logic.propositional.buggy.commimp | 0 | no | p → q ⇏ q → p | |
| logic.propositional.buggy.defimpl.inv | 0 | no | (¬p) ∧ q ⇏ p → q p ∨ (¬q) ⇏ p → q p ∧ (¬q) ⇏ q → p (¬p) ∨ q ⇏ q → p ¬(p ∨ q) ⇏ p → q | |
| logic.propositional.buggy.demorgan1 | 0 | no | ¬(p ∧ q) ⇏ (¬p) ∨ q ¬(p ∧ q) ⇏ p ∨ (¬q) ¬(p ∧ q) ⇏ p ∨ q ¬(p ∨ q) ⇏ (¬p) ∧ q ¬(p ∨ q) ⇏ p ∧ (¬q) ¬(p ∨ q) ⇏ p ∧ q | |
| logic.propositional.buggy.demorgan2 | 0 | no | ¬(p ∧ q) ⇏ ¬((¬p) ∨ (¬q)) ¬(p ∨ q) ⇏ ¬((¬p) ∧ (¬q)) | |
| logic.propositional.buggy.demorgan3 | 0 | no | ¬(p ∧ q) ⇏ (¬p) ∧ (¬q) | |
| logic.propositional.buggy.demorgan3.inv | 0 | no | (¬p) ∧ (¬q) ⇏ ¬(p ∧ q) | |
| logic.propositional.buggy.demorgan4 | 0 | no | ¬(p ∨ q) ⇏ (¬p) ∨ (¬q) | |
| logic.propositional.buggy.demorgan4.inv | 0 | no | (¬p) ∨ (¬q) ⇏ ¬(p ∨ q) | |
| logic.propositional.buggy.demorgan5 | 0 | no | ¬((¬(p ∧ q)) ∨ r) ⇏ (¬((¬p) ∨ (¬q))) ∨ r ¬((¬(p ∧ q)) ∧ r) ⇏ (¬((¬p) ∨ (¬q))) ∧ r ¬((¬(p ∨ q)) ∨ r) ⇏ (¬((¬p) ∧ (¬q))) ∨ r ¬((¬(p ∨ q)) ∧ r) ⇏ (¬((¬p) ∧ (¬q))) ∧ r | |
| logic.propositional.buggy.distr | 0 | no | p ∧ (q ∨ r) ⇏ (p ∧ q) ∧ (p ∧ r) (p ∨ q) ∧ r ⇏ (p ∧ r) ∧ (q ∧ r) p ∧ (q ∨ r) ⇏ (p ∨ q) ∧ (p ∨ r) (p ∨ q) ∧ r ⇏ (p ∨ r) ∧ (q ∨ r) p ∨ (q ∧ r) ⇏ (p ∨ q) ∨ (p ∨ r) (p ∧ q) ∨ r ⇏ (p ∨ r) ∨ (q ∨ r) p ∨ (q ∧ r) ⇏ (p ∧ q) ∨ (p ∧ r) (p ∧ q) ∨ r ⇏ (p ∧ r) ∨ (q ∧ r) | |
| logic.propositional.buggy.distr.inv | 0 | no | (p ∧ q) ∧ (p ∧ r) ⇏ p ∧ (q ∨ r) (p ∧ r) ∧ (q ∧ r) ⇏ (p ∨ q) ∧ r (p ∨ q) ∧ (p ∨ r) ⇏ p ∧ (q ∨ r) (p ∨ r) ∧ (q ∨ r) ⇏ (p ∨ q) ∧ r (p ∨ q) ∨ (p ∨ r) ⇏ p ∨ (q ∧ r) (p ∨ r) ∨ (q ∨ r) ⇏ (p ∧ q) ∨ r (p ∧ q) ∨ (p ∧ r) ⇏ p ∨ (q ∧ r) (p ∧ r) ∨ (q ∧ r) ⇏ (p ∧ q) ∨ r | |
| logic.propositional.buggy.distrnot | 0 | no | (¬p) ∧ (q ∨ r) ⇏ ((¬p) ∧ q) ∨ (p ∧ r) (¬p) ∧ (q ∨ r) ⇏ (p ∧ q) ∨ ((¬p) ∧ r) (p ∨ q) ∧ (¬r) ⇏ (p ∧ (¬r)) ∨ (q ∧ r) (p ∨ q) ∧ (¬r) ⇏ (p ∧ r) ∨ (q ∧ (¬r)) (¬p) ∨ (q ∧ r) ⇏ ((¬p) ∨ q) ∧ (p ∨ r) (¬p) ∨ (q ∧ r) ⇏ (p ∨ q) ∧ ((¬p) ∨ r) (p ∧ q) ∨ (¬r) ⇏ (p ∨ (¬r)) ∧ (q ∨ r) (p ∧ q) ∨ (¬r) ⇏ (p ∨ r) ∧ (q ∨ (¬r)) | |
| logic.propositional.buggy.equivelim1 | 0 | no | p ↔ q ⇏ (p ∧ q) ∨ (¬(p ∧ q)) p ↔ q ⇏ (p ∧ q) ∨ ((¬p) ∧ q) p ↔ q ⇏ (p ∧ q) ∨ (p ∧ (¬q)) p ↔ q ⇏ (p ∧ q) ∨ (p ∧ q) p ↔ q ⇏ (p ∧ q) ∨ (¬(p ∨ (¬q))) | |
| logic.propositional.buggy.equivelim2 | 0 | no | p ↔ q ⇏ (p ∨ q) ∧ ((¬p) ∨ (¬q)) p ↔ q ⇏ (p ∧ q) ∧ ((¬p) ∧ (¬q)) p ↔ q ⇏ (p ∧ q) ∨ ((¬p) ∨ (¬q)) | |
| logic.propositional.buggy.equivelim3 | 0 | no | p ↔ q ⇏ (¬p) ∨ q | |
| logic.propositional.buggy.falseprop | 0 | no | p ∨ F ⇏ F F ∨ p ⇏ F p ∧ F ⇏ p F ∧ p ⇏ p | |
| logic.propositional.buggy.falseprop.inv | 0 | no | ||
| logic.propositional.buggy.idemequi | 0 | no | p ↔ p ⇏ p | |
| logic.propositional.buggy.idemequiv.inv | 0 | no | p ⇏ p ↔ p | |
| logic.propositional.buggy.idemimp | 0 | no | p → p ⇏ p | |
| logic.propositional.buggy.idemimp.inv | 0 | no | p ⇏ p → p | |
| logic.propositional.buggy.implelim | 0 | no | p → q ⇏ ¬(p ∨ q) p → q ⇏ p ∨ q p → q ⇏ ¬(p ∧ q) p → q ⇏ p ∨ (¬q) | |
| logic.propositional.buggy.implelim1 | 0 | no | p → q ⇏ (¬p) ∧ q | |
| logic.propositional.buggy.implelim2 | 0 | no | p → q ⇏ (p ∧ q) ∨ ((¬p) ∧ (¬q)) | |
| logic.propositional.buggy.notoverimpl | 0 | no | ¬(p → q) ⇏ (¬p) → (¬q) | |
| logic.propositional.buggy.orcompl | 0 | no | p ∨ (¬p) ⇏ F (¬p) ∨ p ⇏ F p ∨ (¬p) ⇏ p (¬p) ∨ p ⇏ p | |
| logic.propositional.buggy.orcompl.inv | 0 | no | ||
| logic.propositional.buggy.orsame | 0 | no | p ∨ p ⇏ T | |
| logic.propositional.buggy.parenth1 | 0 | no | ¬(p ∧ q) ⇏ (¬p) ∧ q ¬(p ∨ q) ⇏ (¬p) ∨ q | |
| logic.propositional.buggy.parenth2 | 0 | no | ¬(p ↔ q) ⇏ (¬(p ∧ q)) ∨ ((¬p) ∧ (¬q)) | |
| logic.propositional.buggy.parenth3 | 0 | no | ¬((¬p) ∧ q) ⇏ p ∧ q ¬((¬p) ∨ q) ⇏ p ∨ q ¬((¬p) → q) ⇏ p → q ¬((¬p) ↔ q) ⇏ p ↔ q | |
| logic.propositional.buggy.trueprop | 0 | no | p ∨ T ⇏ p T ∨ p ⇏ p p ∧ T ⇏ T T ∧ p ⇏ T | |
| logic.propositional.buggy.trueprop.inv | 0 | no |