Also known as KT4 this logic add the following axioms to K:
T = []p -> p which forces the Kripke reachability relation to be reflexive
4 = []p -> [][]p which forces the Kripke reachability relation to be transitive.
It is characterised by finite rooted transitive trees of clusters where a cluster
is a finite set of points with every world in the cluster reachable from every other world in the cluster.
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.