true. More technically, modal tableaux methods check the existence of a model and a world that make set of formulae true. If are true in , there must be a world that is accessible from and that makes true. This rule therefore amounts to deriving a set of formulae that must be satisfied in such . While the preconditions are assumed satisfied by , the consequences are assumed satisfied in : same model but possibly different worlds. Set-labeled tableaux do not explicitly keep track of the world where each formula is assumed true: two nodes may or may not refer to the same world. However, the formulae labeling any given node are assumed true at the same world. As a result of the possibly different worlds where formulae are assumed true, a formula in a node is not automatically valid in all its descendants, as every application of the modal rule corresponds to a move from a world to another one. This condition is automatically captured by set-labeling tableaux, as expansion rules are based only on the leaf where they are applied and not on its ancestors. Notably, does not directly extend to multiple negated boxed formulae such as in : while there exists an accessible world where is false and one in which is false, these two worlds are not necessarily the same. Differently from the propositional rules, states conditions over all its preconditions. For example, it cannot be applied to a node labeled by ; while this set is inconsistent and this could be easily proved by applying , this rule cannot be applied because of formula , which is not even relevant to inconsistency. Removal of such formulae is made possible by the rule: The addition of this rule (thinning rule) makes the resulting calculus non-confluent: a tableau for an inconsistent set may be impossible to close, even if a closed tableau for the same set exists. Rule is non-deterministic: the set of formulae to be removed (or to be kept) can be chosen arbitrarily; this creates the problem of choosing a set of formulae to discard that is not so large it makes the resulting set satisfiable and not so small it makes the necessary expansion rules inapplicable. Having a large number of possible choices makes the problem of searching for a closed tableau harder. This non-determinism can be avoided by restricting the usage of so