This is the web interface of GenZ.

Please choose a logic: CPL IPL D D4 D45 GL K K4 K45 S4 T and a data structure: zipper tree

Enter a formula below using this syntax or choose an example: p → p p → ¬¬p p ↔ ¬¬p p → p p → ¬¬p p ↔ ¬¬p ¬¬(p | ¬p) (p → q) → ⊥ ☐p → ◇p ☐p → ☐☐◇p ◇p → □◇p ☐(☐p → p) → ☐p ☐(p1 & p2) → (☐p1 | ☐p2) ¬◇false ☐☐☐☐true ¬¬¬¬false ☐p1 → ☐☐p1 ☐☐p → ☐p ☐☐☐☐☐☐p → ☐☐☐p ◇□p | □◇□p ☐☐p → ☐p p → ◇p ☐(☐p → ⊥) → ☐(p → ⊥) ☐(☐p → ⊥) → ☐q ◇p → □◇p □□p → □p □p → □□p □p → p p → □p

| Symbols            | Meaning                 | Note                             |
|--------------------|-------------------------|----------------------------------|
| p, q, bla, ...     | atomic propositions     |                                  |
| true, ⊤            | top (constant true)     |                                  |
| false, ⊥           | bottom (constant false) |                                  |
| !, ~, ¬            | negation (not)          | abreviation for ... -> false     |
| &                  | conjunction (and)       | primitive                        |
| |, v               | disjunction (or)        | primitive                        |
| ->, -->, =>, →     | implication (if-then)   | primitive                        |
| <->, <-->, <=>, ↔  | bi-implication (iff)    | abbreviation using -> and &      |
| <>, <a>, ◇         | diamond (possible)      | abbreviation for ~ [] ~ ...      |
| [], [a], ☐, ◻      | box (necessary)         | primitive                        |