world of the same model. A related problem is the global consequence problem, where the assumption is that a formula (or set of formulae) is true in all possible worlds of the model. The problem is that of checking whether, in all models where is true in all worlds, is also true in all worlds. Local and global assumption differ on models where the assumed formula is true in some worlds but not in others. As an example, entails globally but not locally. Local entailment does not hold in a model consisting of two worlds making and true, respectively, and where the second is accessible from the first; in the first world, the assumptions are true but is false. This counterexample works because can be assumed true in a world and false in another one. If however the same assumption is considered global, is not allowed in any world of the model. These two problems can be combined, so that one can check whether is a local consequence of under the global assumption . Tableaux calculi can deal with global assumption by a rule allowing its addition to every node, regardless of the world it refers to. Notations The following conventions are sometimes used. Uniform notation When writing tableaux expansion rules, formulae are often denoted using a convention, so that for example is always considered to be . The following table provides the notation for formulae in propositional, first-order, and modal logic. Each label in the first column is taken to be either formula in the other columns. An overlined formula such as indicates that is the negation of whatever formula appears in its place, so that for example in formula the subformula is the negation of . Since every label indicates many equivalent formulae, this notation allows writing a single rule for all these equivalent formulae. For example, the conjunction expansion rule is formulated as: Signed formulae A formula in a tableau is assumed true. Signed tableaux allows stating that a formula is false. This is generally achieved by adding a label to each formula, where the label T indicates formulae assumed true and F those assumed false. A different but equivalent notation is that to write formulae that are assumed true at the left of the node and formulae assumed false at its right. History In his Symbolic Logic Part II, Charles Lutwidge Dodgson (also known by his