that it is only applied before a modal expansion rule, and so that it only removes the formulae that make that other rule inapplicable. This condition can be also formulated by merging the two rules in a single one. The resulting rule produces the same result as the old one, but implicitly discard all formulae that made the old rule inapplicable. This mechanism for removing has been proved to preserve completeness for many modal logics. Axiom T expresses reflexivity of the accessibility relation: every world is accessible from itself. The corresponding tableau expansion rule is: This rule relates conditions over the same world: if is true in a world, by reflexivity is also true in the same world. This rule is static, not transactional, as both its precondition and consequent refer to the same world. This rule copies from the precondition to the consequent, in spite of this formula having been "used" to generate . This is correct, as the considered world is the same, so also holds there. This "copying" is necessary in some cases. It is for example necessary to prove the inconsistency of : the only applicable rules are in order , from which one is blocked if is not copied. Auxiliary tableaux A different method for dealing with formulae holding in alternate worlds is to start a different tableau for each new world that is introduced in the tableau. For example, implies that is false in an accessible world, so one starts a new tableau rooted by . This new tableau is attached to the node of the original tableau where the expansion rule has been applied; a closure of this tableau immediately generates a closure of all branches where that node is, regardless of whether the same node is associated other auxiliary tableaux. The expansion rules for the auxiliary tableaux are the same as for the original one; therefore, an auxiliary tableau can have in turns other (sub-)auxiliary tableaux. Global assumptions The above modal tableaux establish the consistency of a set of formulae, and can be used for solving the local logical consequence problem. This is the problem of telling whether, for each model , if is true in a world , then is also true in the same world. This is the same as checking whether is true in a world of a model, in the assumption that is also true in the same