all formulae , as these hold in the new world as well. In order to retain completeness, the deleted formulae are then added to all other branches that still refer to the old world. World-labeled tableau A different mechanism for ensuring the correct interaction between formulae referring to different worlds is to switch from formulae to labeled formulae: instead of writing , one would write to make it explicit that holds in world . All propositional expansion rules are adapted to this variant by stating that they all refer to formulae with the same world label. For example, generates two nodes labeled with and ; a branch is closed only if it contains two opposite literals of the same world, like and ; no closure is generated if the two world labels are different, like in and . A modal expansion rule may have a consequence that refers to different worlds. For example, the rule for would be written as follows The precondition and consequent of this rule refer to worlds and , respectively. The various calculi use different methods for keeping track of the accessibility of the worlds used as labels. Some include pseudo-formulae like to denote that is accessible from . Some others use sequences of integers as world labels, this notation implicitly representing the accessibility relation (for example, is accessible from .) Set-labeling tableaux The problem of interaction between formulae holding in different worlds can be overcome by using set-labeling tableaux. These are trees whose nodes are labeled with sets of formulae; the expansion rules explain how to attach new nodes to a leaf, based only on the label of the leaf (and not on the label of other nodes in the branch). Tableaux for modal logics are used to verify the satisfiability of a set of modal formulae in a given modal logic. Given a set of formulae , they check the existence of a model and a world such that . The expansion rules depend on the particular modal logic used. A tableau system for the basic modal logic K can be obtained by adding to the propositional tableau rules the following one: Intuitively, the precondition of this rule expresses the truth of all formulae at all accessible worlds, and truth of at some accessible worlds. The consequence of this rule is a formula that must be true at one of those worlds where is