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 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