There are 9 decomposition rules. There is one for each of the 4 binary operators; one for each denial of one the 4 binary operators; and one for double negations. The 9 are shown in their respective decomposition editor tables.
Note: In the editor tables, left, same, and right refer to the possible branches columns into which an existing branch may grow.
| A • B | ~(A • B) | ||||||
| Left | Same | Right | Left | Same | Right | ||
| A | A | ||||||
| ~A | ~A | ||||||
| B | B | ||||||
| ~B | ~B |
| A∨B | ~(A∨B) | ||||||
| Left | Same | Right | Left | Same | Right | ||
| A | A | ||||||
| ~A | ~A | ||||||
| B | B | ||||||
| ~B | ~B |
| A⊃B | ~(A⊃B) | ||||||
| Left | Same | Right | Left | Same | Right | ||
| A | A | ||||||
| ~A | ~A | ||||||
| B | B | ||||||
| ~B | ~B |
| A ≡ B | ~(A ≡ B) | ||||||
| Left | Same | Right | Left | Same | Right | ||
| A | A | A | |||||
| ~A | ~A | ~A | |||||
| B | B | B | |||||
| ~B | ~B | ~B |
| ~~A | |||
| Left | Same | Right | |
| A | |||
| ~A | |||
| A | |||
| ~A | |||
| A | A |
Any one of the three A's can be selected. Note: A fifth row may also appear in other editor tables.