world, but also on the ones that are accessible from it. As an example, is true in a world if is true in all worlds that are accessible from it. As for propositional logic, tableaux for modal logics are based on recursively breaking formulae into its basic components. Expanding a modal formula may however require stating conditions over different worlds. As an example, if is true in a world then there exists a world accessible from it where is false. However, one cannot simply add the following rule to the propositional ones. In propositional tableaux all formulae refer to the same truth evaluation, but the precondition of the rule above holds in one world while the consequence holds in another. Not taking into account this would generate incorrect results. For example, formula states that is true in the current world and is false in a world that is accessible from it. Simply applying and the expansion rule above would produce and , but these two formulae should not in general generate a contradiction, as they hold in different worlds. Modal tableaux calculi do contain rules of the kind of the one above, but include mechanisms to avoid the incorrect interaction of formulae referring to different worlds. Technically, tableaux for modal logics check the satisfiability of a set of formulae: they check whether there exists a model and world such that the formulae in the set are true in that model and world. In the example above, while states the truth of in , the formula states the truth of in some world that is accessible from and which may in general be different from . Tableaux calculi for modal logic take into account that formulae may refer to different worlds. This fact has an important consequence: formulae that hold in a world may imply conditions over different successors of that world. Unsatisfiability may then be proved from the subset of formulae referring to a single successor. This holds if a world may have more than one successor, which is true for most modal logics. If this is the case, a formula like is true if a successor where holds exists and a successor where holds exists. In the other way around, if one can show unsatisfiability of in an arbitrary successor, the formula is proved unsatisfiable without checking for worlds where holds. At the same time, if one can show