Exercise relationalgebra.cnf
Description
To conjunctive normal form
Rules for relationalgebra.cnf
| Rule name | Args | Used | Siblings | Rewrite rule |
| relationalgebra.absorp | 0 | yes | r ∩ (r ∪ s) ⇒ r r ∩ (s ∪ r) ⇒ r (r ∪ s) ∩ r ⇒ r (s ∪ r) ∩ r ⇒ r r ∪ (r ∩ s) ⇒ r r ∪ (s ∩ r) ⇒ r (r ∩ s) ∪ r ⇒ r (s ∩ r) ∪ r ⇒ r | |
| relationalgebra.absorpcompl | 0 | yes | r ∩ ((r‾) ∪ s) ⇒ r ∩ s r ∩ (s ∪ (r‾)) ⇒ r ∩ s ((r‾) ∪ s) ∩ r ⇒ r ∩ s (s ∪ (r‾)) ∩ r ⇒ r ∩ s r ∪ ((r‾) ∩ s) ⇒ r ∪ s r ∪ (s ∩ (r‾)) ⇒ r ∪ s ((r‾) ∩ s) ∪ r ⇒ r ∪ s (s ∩ (r‾)) ∪ r ⇒ r ∪ s | |
| relationalgebra.addoverintersec | 0 | yes | r † (s ∩ t) ⇒ (r † s) ∩ (r † t) (r ∩ s) † t ⇒ (r † t) ∩ (s † t) | |
| relationalgebra.compoverunion | 0 | yes | r ; (s ∪ t) ⇒ (r ; s) ∪ (r ; t) (r ∪ s) ; t ⇒ (r ; t) ∪ (s ; t) | |
| relationalgebra.demorganand | 0 | yes | (r ∩ s)‾ ⇒ (r‾) ∪ (s‾) | |
| relationalgebra.demorganor | 0 | yes | (r ∪ s)‾ ⇒ (r‾) ∩ (s‾) | |
| relationalgebra.doubleinv | 0 | yes | (r~)~ ⇒ r | |
| relationalgebra.doublenegation | 0 | yes | (r‾)‾ ⇒ r | |
| relationalgebra.idempotencyand | 0 | yes | r ∩ r ⇒ r | |
| relationalgebra.idempotencyor | 0 | yes | r ∪ r ⇒ r | |
| relationalgebra.invoveradd | 0 | yes | (r † s)~ ⇒ (s~) † (r~) | |
| relationalgebra.invovercomp | 0 | yes | (r ; s)~ ⇒ (s~) ; (r~) | |
| relationalgebra.invoverintersect | 0 | yes | (r ∩ s)~ ⇒ (r~) ∩ (s~) | |
| relationalgebra.invovernot | 0 | yes | (r‾)~ ⇒ (r~)‾ | |
| relationalgebra.invoverunion | 0 | yes | (r ∪ s)~ ⇒ (r~) ∪ (s~) | |
| relationalgebra.notoveradd | 0 | yes | (r † s)‾ ⇒ (r‾) ; (s‾) | |
| relationalgebra.notovercomp | 0 | yes | (r ; s)‾ ⇒ (r‾) † (s‾) | |
| relationalgebra.remcompl | 0 | yes | r ∪ (r‾) ⇒ V (r‾) ∪ r ⇒ V r ∩ (r‾) ⇒ V‾ (r‾) ∩ r ⇒ V‾ | |
| relationalgebra.remredunexprs | 0 | yes | r ∪ V ⇒ V V ∪ r ⇒ V r ∩ V ⇒ r V ∩ r ⇒ r V ; V ⇒ V r † V ⇒ V V † r ⇒ V V~ ⇒ V (V‾)~ ⇒ V‾ r ∪ (V‾) ⇒ r (V‾) ∪ r ⇒ r r ∩ (V‾) ⇒ V‾ (V‾) ∩ r ⇒ V‾ r ; (V‾) ⇒ V‾ (V‾) ; r ⇒ V‾ (V‾) † (V‾) ⇒ V‾ I~ ⇒ I I ; r ⇒ r r ; I ⇒ r | |
| relationalgebra.unionoverintersec | 0 | yes | r ∪ (s ∩ t) ⇒ (r ∪ s) ∩ (r ∪ t) (r ∩ s) ∪ t ⇒ (r ∪ t) ∩ (s ∪ t) |
Buggy rules for relationalgebra.cnf
| Rule name | Args | Used | Siblings | Rewrite rule |
| relationalgebra.buggy.addoverunion | 0 | no | r † (s ∪ t) ⇏ (r † s) ∪ (r † t) (r ∪ s) † t ⇏ (r † t) ∪ (s † t) | |
| relationalgebra.buggy.assoc | 0 | no | r ∪ (s ∩ t) ⇏ (r ∪ s) ∩ t (r ∪ s) ∩ t ⇏ r ∪ (s ∩ t) (r ∩ s) ∪ t ⇏ r ∩ (s ∪ t) r ∩ (s ∪ t) ⇏ (r ∩ s) ∪ t r ; (s ∪ t) ⇏ (r ; s) ∪ t (r ∪ s) ; t ⇏ r ∪ (s ; t) r ; (s ∩ t) ⇏ (r ; s) ∩ t (r ∩ s) ; t ⇏ r ∩ (s ; t) r † (s ∪ t) ⇏ (r † s) ∪ t (r ∪ s) † t ⇏ r ∪ (s † t) r † (s ∩ t) ⇏ (r † s) ∩ t (r ∩ s) † t ⇏ r ∩ (s † t) | |
| relationalgebra.buggy.compoverintersec | 0 | no | r ; (s ∩ t) ⇏ (r ; s) ∩ (r ; t) (r ∩ s) ; t ⇏ (r ; t) ∩ (s ; t) | |
| relationalgebra.buggy.demorgan | 0 | no | (r ∩ s)‾ ⇏ (r‾) ∪ s (r ∩ s)‾ ⇏ r ∪ (s‾) (r ∩ s)‾ ⇏ ((r‾) ∪ (s‾))‾ (r ∪ s)‾ ⇏ (r‾) ∩ s (r ∪ s)‾ ⇏ r ∩ (s‾) (r ∪ s)‾ ⇏ ((r‾) ∩ (s‾))‾ | |
| relationalgebra.buggy.idemadd | 0 | no | r † r ⇏ r | |
| relationalgebra.buggy.idemcomp | 0 | no | r ; r ⇏ r | |
| relationalgebra.buggy.invoveradd | 0 | no | (r † s)~ ⇏ (r~) † (s~) | |
| relationalgebra.buggy.invovercomp | 0 | no | (r ; s)~ ⇏ (r~) ; (s~) | |
| relationalgebra.buggy.notoveradd | 0 | no | (r † s)‾ ⇏ (r‾) † (s‾) (r † s)‾ ⇏ (r‾) ; s (r † s)‾ ⇏ (r‾) † s (r † s)‾ ⇏ ((r‾) ; (s‾))‾ | |
| relationalgebra.buggy.notovercomp | 0 | no | (r ; s)‾ ⇏ (r‾) ; (s‾) (r ; s)‾ ⇏ (r‾) ; s (r ; s)‾ ⇏ (r‾) † s (r ; s)‾ ⇏ ((r‾) ; (s‾))‾ | |
| relationalgebra.buggy.parenth | 0 | no | (r ∩ s)‾ ⇏ (r‾) ∩ s (r ∪ s)‾ ⇏ (r‾) ∪ s ((r‾) ∩ s)‾ ⇏ r ∩ s ((r‾) ∪ s)‾ ⇏ r ∪ s ((r‾) ; s)‾ ⇏ r ; s ((r‾) † s)‾ ⇏ r † s (r ∩ s)~ ⇏ (r~) ∩ s (r ∪ s)~ ⇏ (r~) ∪ s ((r~) ∩ s)~ ⇏ r ∩ s ((r~) ∪ s)~ ⇏ r ∪ s ((r~) ; s)~ ⇏ r ; s ((r~) † s)~ ⇏ r † s | |
| relationalgebra.buggy.remcompl | 0 | no | r ∩ (r‾) ⇏ V (r‾) ∩ r ⇏ V r ∪ (r‾) ⇏ V‾ (r‾) ∪ r ⇏ V‾ |