Propositional Modal Logic K4

K4 has the following axion on top of normal modal logic K:
[]p -> [][]p which enforces that the Kripke reachability relation R is transitive.

When you enter a formula A, then "closed" means that A is a
theorem because the tableau for ~ A is closed, and "open" means
that it is not a theorem because the tableau for ~ A is open.

Results
Query
Info