The basic normal modal logic K is characterised by the set of all Kripke frames with a binary reachability

relation. Its decision problem is PSPACE complete.

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.