text:
Method of analytic tableaux

In proof theory, the semantic tableau (plural: tableaux), also called an analytic tableau, truth tree, or simply tree, is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics.

A method of truth trees contains a fixed set of rules for producing trees from a given logical formula, or set of logical formulas. Those trees will have more formulas at each branch, and in some cases, a branch can come to contain both a formula and its negation, which is to say, a contradiction. In that case, the branch is said to close. If every branch in a tree closes, the tree itself is said to close. In virtue of the rules for construction of tableaux, a closed tree is a proof that the original formula, or set of formulas, used to construct it was itself self-contradictory, and therefore false. Conversely, a tableau can also prove that a logical formula is tautologous: if a formula is tautologous, its negation is a contradiction, so a tableau built from its negation will close.

History
In his Symbolic Logic Part II, Charles Lutwidge Dodgson (also known by his literary pseudonym, Lewis Carroll) introduced the Method of Trees, the earliest modern use of a truth tree.

The method of semantic tableaux was invented by the Dutch logician Evert Willem Beth (Beth 1955) and simplified, for classical logic, by Raymond Smullyan (Smullyan 1968, 1995). Smullyan's simplification, "one-sided tableaux", is described here. Smullyan's method has been generalized to arbitrary many-valued propositional and first-order logics by Walter Carnielli (Carnielli 1987).

Tableaux can be intuitively seen as sequent systems upside-down. This symmetrical relation between tableaux and sequent systems was formally established in (Carnielli 1991).

Background
A formula in propositional logic consists of letters, which stand for propositions, and connectives for conjunction, disjunction, conditionals, biconditionals, and negation. The truth or falsehood of a proposition is called its truth value. A formula, or set of formulas, is said to be satisfiable if there is a possible assignment of truth-values to the propositional letters such that the entire formula, which combines the letters with connectives, is itself true as well. Such an assignment is said to satisfy the formula.

A tableau checks whether a given set of formulae is satisfiable or not. It can be used to check either validity or entailment: a formula is valid if its negation is unsatisfiable, and formulae $$A_1,\ldots,A_n$$ imply $$B$$ if $$\{A_1,\ldots,A_n,\neg B\}$$ is unsatisfiable.

The following table shows some notational variants for logical connectives, for readers who may be more familiar with a different notation from the one used here. In general, as of the time of the inclusion of this sentence, the first symbol in each line has been used in the text of this article; however, since Wikipedia editors are not rule-bound to use consistent notation within or between articles, this may change.

General method
The main principle of propositional tableaux is to attempt to "break" complex formulae into smaller ones until complementary pairs of literals are produced or no further expansion is possible.

The method works on a tree whose nodes are labeled with formulae. At each step, this tree is modified; in the propositional case, the only allowed changes are additions of a node as descendant of a leaf. The procedure starts by generating the tree made of a chain of all formulae in the set to prove unsatisfiability. Then, the following procedure may be repeatedly applied nondeterministically:

 * 1) Pick an open leaf node. (The leaf node in the initial chain is marked open).
 * 2) Pick an applicable node on the branch above the selected node.
 * 3) Apply the applicable node, which corresponds to expanding the tree below the selected leaf node based on some expansion rule (detailed below).
 * 4) For every newly created node that is both a literal/negated literal, and whose complement appears in a prior node on the same branch, mark the branch as closed. Mark all other newly created nodes as open.

Eventually, this procedure will terminate, because at some point every applicable node gets applied, and the expansion rules guarantee that every node in the tree is simpler than the applicable node used to create it.

The principle of tableau is that formulae in nodes of the same branch are considered in conjunction while the different branches are considered to be disjuncted. As a result, a tableau is a tree-like representation of a formula that is a disjunction of conjunctions. This formula is equivalent to the set to prove unsatisfiability. The procedure modifies the tableau in such a way that the formula represented by the resulting tableau is equivalent to the original one. One of these conjunctions may contain a pair of complementary literals, in which case that conjunction is proved to be unsatisfiable. If all conjunctions are proved unsatisfiable, the original set of formulae is unsatisfiable.

And
Whenever a branch of a tableau contains a formula $$A \wedge B$$ that is the conjunction of two formulae, these two formulae are both consequences of that formula. This fact can be formalized by the following rule for expansion of a tableau:

($$\wedge$$) If a branch of the tableau contains a conjunctive formula $$A \wedge B$$, add to its leaf the chain of two nodes containing the formulae $$A$$ and $$B$$

This rule is generally written as follows:

 * $$(\land) \frac{A \wedge B}{\begin{array}{c} A \\ B\end{array}}$$

A variant of this rule allows a node to contain a set of formulae rather than a single one. In this case, the formulae in this set are considered in conjunction, so one can add $$\{A, B\}$$ at the end of a branch containing $$A \wedge B$$. More precisely, if a node on a branch is labeled $$X \cup \{A \wedge B\}$$, one can add to the branch the new leaf $$X \cup \{A, B\}$$.

Or
If a branch of a tableau contains a formula that is a disjunction of two formulae, such as $$A \vee B$$, the following rule can be applied:

($$\vee$$) If a node on a branch contains a disjunctive formula $$A \vee B$$, then create two sibling children to the leaf of the branch, containing the formulae $$A$$ and $$B$$, respectively.

This rule splits a branch into two, differing only for the final node. Since branches are considered in disjunction to each other, the two resulting branches are equivalent to the original one, as the disjunction of their non-common nodes is precisely $$A \vee B$$. The rule for disjunction is generally formally written using the symbol $$|$$ for separating the formulae of the two distinct nodes to be created:

 * $$(\vee) \frac{A \vee B}{A\mid B}$$

If nodes are assumed to contain sets of formulae, this rule is replaced by: if a node is labeled $$Y \cup \{A \vee B\}$$, a leaf of the branch this node is in can be appended two sibling child nodes labeled $$Y \cup \{A\}$$ and $$Y \cup \{B\}$$, respectively.

Not
The aim of tableaux is to generate progressively simpler formulae until pairs of opposite literals are produced or no other rule can be applied. Negation can be treated by initially making formulae in negation normal form, so that negation only occurs in front of literals. Alternatively, one can use De Morgan's laws during the expansion of the tableau, so that for example $$\neg (A \wedge B)$$ is treated as $$\neg A \vee \neg B$$. Rules that introduce or remove a pair of negations (such as in $$\neg \neg A$$) are also used in this case (otherwise, there would be no way of expanding a formula like $$\neg \neg (A \wedge B) )$$:

 * $$(\neg 1) \frac{A}{\neg \neg A}$$

 * $$(\neg 2) \frac{\neg \neg A}{A}$$

Closure
Every tableau can be considered as a graphical representation of a formula, which is equivalent to the set the tableau is built from. This formula is as follows: each branch of the tableau represents the conjunction of its formulae; the tableau represents the disjunction of its branches. The expansion rules transforms a tableau into one having an equivalent represented formula. Since the tableau is initialized as a single branch containing the formulae of the input set, all subsequent tableaux obtained from it represent formulae which are equivalent to that set (in the variant where the initial tableau is the single node labeled true, the formulae represented by tableaux are consequences of the original set.)

The method of tableaux works by starting with the initial set of formulae and then adding to the tableau simpler and simpler formulae until contradiction is shown in the simple form of opposite literals. Since the formula represented by a tableau is the disjunction of the formulae represented by its branches, contradiction is obtained when every branch contains a pair of opposite literals. Once a branch contains a literal and its negation, its corresponding formula is unsatisfiable. As a result, this branch can be now "closed", as there is no need to further expand it. If all branches of a tableau are closed, the formula represented by the tableau is unsatisfiable; therefore, the original set is unsatisfiable as well. Obtaining a tableau where all branches are closed is a way for proving the unsatisfiability of the original set. In the propositional case, one can also prove that satisfiability is proved by the impossibility of finding a closed tableau, provided that every expansion rule has been applied everywhere it could be applied. In particular, if a tableau contains some open (non-closed) branches and every formula that is not a literal has been used by a rule to generate a new node on every branch the formula is in, the set is satisfiable.

This rule takes into account that a formula may occur in more than one branch (this is the case if there is at least a branching point "below" the node). In this case, the rule for expanding the formula has to be applied so that its conclusion(s) are appended to all of these branches that are still open, before one can conclude that the tableau cannot be further expanded and that the formula is therefore satisfiable.

Set-labeled tableau
A variant of tableau is to label nodes with sets of formulae rather than single formulae. In this case, the initial tableau is a single node labeled with the set to be proved satisfiable. The formulae in a set are therefore considered to be in conjunction.

The rules of expansion of the tableau can now work on the leaves of the tableau, ignoring all internal nodes. For conjunction, the rule is based on the equivalence of a set containing a conjunction $$A \wedge B$$ with the set containing both $$A$$ and $$B$$ in place of it. In particular, if a leaf is labeled with $$X \cup \{A \wedge B\}$$, a node can be appended to it with label $$X \cup \{A, B\}$$:

 * $$(\wedge) \frac{X \cup \{A \wedge B\}}{X \cup \{A, B\}}$$

For disjunction, a set $$X \cup \{A \vee B\}$$ is equivalent to the disjunction of the two sets $$X \cup \{A\}$$ and $$X \cup \{B\}$$. As a result, if the first set labels a leaf, two children can be appended to it, labeled with the latter two formulae.

 * $$(\vee) \frac{X \cup \{A \vee B\}}{X \cup \{A\}|X \cup \{B\}}$$

Finally, if a set contains both a literal and its negation, this branch can be closed:

 * $$(id) \frac{X \cup \{p, \neg p\}}{closed}$$

A tableau for a given finite set X is a finite (upside down) tree with root X in which all child nodes are obtained by applying the tableau rules to their parents. A branch in such a tableau is closed if its leaf node contains "closed". A tableau is closed if all its branches are closed. A tableau is open if at least one branch is not closed.

Below are two closed tableaux for the set
 * $$X = \{r \wedge \neg r,\; p \wedge ((\neg p \vee q) \wedge \neg q)\}$$

Each rule application is marked at the right hand side. Both achieve the same effect, the first closes faster. The only difference is the order in which the reduction is performed.

\dfrac{\quad \dfrac{ \quad r \wedge \neg r,\; p \wedge ((\neg p \vee q) \wedge \neg q)    \quad }{    r,\; \neg r,\; p \wedge ((\neg p \vee q) \wedge \neg q)   }(\wedge) }{ closed } (\wedge) $$ and second, longer one, with the rules applied in a different order:

\dfrac{ \quad \dfrac { \quad \dfrac {        \quad r \wedge \neg r,\; p \wedge ((\neg p \vee q) \wedge \neg q)        \quad }{         r \wedge \neg r,\; p,\; ((\neg p \vee q) \wedge \neg q)       } (\wedge) \quad }{    r \wedge \neg r,\; p,\;  (\neg p \vee q),\;  \neg q   } (\wedge) }{  \quad \dfrac { \quad r \wedge \neg r,\; p,\; \neg p,\; \neg q    \quad }{    closed } (id) \quad\quad \dfrac { \quad r \wedge \neg r,\; p,\; q,\; \neg q     \quad }{     closed } (id) } (\vee) $$

The first tableau closes after only one rule application while the second one misses the mark and takes a lot longer to close. Clearly, we would prefer to always find the shortest closed tableaux but it can be shown that one single algorithm that finds the shortest closed tableaux for all input sets of formulae cannot exist.

The three rules $$(\wedge)$$, $$(\vee)$$ and $$(id)$$ given above are then enough to decide if a given set $$X'$$ of formulae in negated normal form are jointly satisfiable: Just apply all possible rules in all possible orders until we find a closed tableau for $$X'$$ or until we exhaust all possibilities and conclude that every tableau for $$X'$$ is open. In the first case, $$X'$$ is jointly unsatisfiable and in the second the case the leaf node of the open branch gives an assignment to the atomic formulae and negated atomic formulae which makes $$X'$$ jointly satisfiable. Classical logic actually has the rather nice property that we need to investigate only (any) one tableau completely: if it closes then $$X'$$ is unsatisfiable and if it is open then $$X'$$ is satisfiable. But this property is not generally enjoyed by other logics.

These rules suffice for all of classical logic by taking an initial set of formulae X and replacing each member C by its logically equivalent negated normal form C'  giving a set of formulae X' . We know that X is satisfiable if and only if X'  is satisfiable, so it suffices to search for a closed tableau for X'  using the procedure outlined above.

By setting $$X = \{\neg A\}$$ we can test whether the formula A is a tautology of classical logic: If the tableau for $$\{\neg A\}$$ closes then $$\neg A$$ is unsatisfiable and so A is a tautology since no assignment of truth values will ever make A false. Otherwise any open leaf of any open branch of any open tableau for $$\{\neg A\}$$ gives an assignment that falsifies A.

Conditional
Classical propositional logic usually has a connective to denote material implication. If we write this connective as ⇒, then the formula A ⇒ B stands for "if A then B". It is possible to give a tableau rule for breaking down A ⇒ B into its constituent formulae. Similarly, we can give one rule each for breaking down each of ¬(A ∧ B), ¬(A ∨ B), ¬(¬A), and ¬(A ⇒ B). Together these rules would give a terminating procedure for deciding whether a given set of formulae is simultaneously satisfiable in classical logic since each rule breaks down one formula into its constituents but no rule builds larger formulae out of smaller constituents. Thus we must eventually reach a node that contains only atoms and negations of atoms. If this last node matches (id) then we can close the branch, otherwise it remains open.

But note that the following equivalences hold in classical logic where (...) = (...) means that the left hand side formula is logically equivalent to the right hand side formula:

$$ \begin{array}{lcl} \neg (A \land B)           & = & \neg A \lor \neg B \\ \neg (A \lor B)            & = & \neg A \land \neg B \\ \neg (\neg A)             & = & A \\ \neg (A \Rightarrow B)    & = & A \land \neg B \\ A \Rightarrow B           & = & \neg A \lor B \\ A \Leftrightarrow B       & = & (A \land B) \lor (\neg A \land \neg B) \\ \neg (A \Leftrightarrow B) & = & (A \land \neg B) \lor (\neg A \land B) \end{array} $$

If we start with an arbitrary formula C of classical logic, and apply these equivalences repeatedly to replace the left hand sides with the right hand sides in C, then we will obtain a formula C'  which is logically equivalent to C but which has the property that C'  contains no implications, and ¬ appears in front of atomic formulae only. Such a formula is said to be in negation normal form and it is possible to prove formally that every formula C of classical logic has a logically equivalent formula C'  in negation normal form. That is, C is satisfiable if and only if C'  is satisfiable.

Propositional tableau with unification
The above rules for propositional tableau can be simplified by using uniform notation. In uniform notation, each formula is either of type $$\alpha $$ (alpha) or of type $$\beta $$ (beta). Each formula of type alpha is assigned the two components $$\alpha_1, \alpha_2$$, and each formula of type beta is assigned the two components $$\beta_1, \beta_2$$. Formulae of type alpha can be thought of as being conjunctive, as both $$\alpha_1$$ and $$\alpha_2$$ are implied by $$\alpha$$ being true. Formulae of type beta can be thought of as being disjunctive, as either $$\beta_1$$ or $$\beta_2$$ is implied by $$\beta$$ being true. The below tables shows how to determine the type, and the components, of any given propositional formula:

$$\begin{array}{c|c|c} \alpha & \alpha_1 & \alpha_2 \\ \hline X \wedge Y&X&Y \\ \neg(X \vee Y)&\neg X&\neg Y\\ \neg(X \implies Y)&X&\neg Y\\ \neg\neg X&X&X\\ \end{array}$$      $$\begin{array}{c|c|c} \beta & \beta_1 & \beta_2 \\ \hline \neg(X \wedge Y)&\neg X&\neg Y \\ X \vee Y&X&Y\\ X \implies Y&\neg X&Y\\ \neg\neg X&X&X\\ \end{array}$$

In each table, the left-most column shows all the possible structures for the formulae of type alpha or beta, and the right-most columns show their respective components. Alternatively, the rules for uniform notation can be expressed using signed formulae:

$$\begin{array}{c|c|c} \alpha & \alpha_1 & \alpha_2 \\ \hline T\,X \wedge Y&T\,\,X&T\,\,Y\\ F\,\,X \vee Y&F\,\,X&F\,\,Y\\ F\,\,X \implies Y&T\,\,X&F\,\,Y\\ F\,\,\neg X&T\,\,X&T\,\,Y\\ T\,\,\neg X&F\,\,X&F\,\,Y\end{array} \qquad \begin{array}{c|c|c} \beta & \beta_1 & \beta_2 \\ \hline F\,\,X \wedge Y&F\,\,Y&F\,\,X\\ T\,\,X \vee Y&T\,\,X&T\,\,Y \\ T\,\,X \implies Y&F\,\,X&T\,\,Y\\ F\,\,\neg X&T\,\,X&T\,\,X\\ T\,\,\neg X&F\,\,X&F\,\,Y\end{array}$$

When constructing a propositional tableau using the above notation, whenever one encounters a formula of type alpha, its two components $$\alpha_1,\alpha_2$$ are added to the current branch that is being expanded. Whenever one encounters a formula of type beta on some branch $$\theta $$, one can split $$\theta $$ into two branches, one with the set {$$\theta $$, $$\beta_1$$} of formulae, and the other with the set {$$\theta $$, $$\beta_2$$} of formulae.

First-order logic tableau
Tableaux are extended to first-order predicate logic by two rules for dealing with universal and existential quantifiers, respectively. Two different sets of rules can be used; both employ a form of Skolemization for handling existential quantifiers, but differ on the handling of universal quantifiers.

The set of formulae to check for validity is here supposed to contain no free variables; this is not a limitation as free variables are implicitly universally quantified, so universal quantifiers over these variables can be added, resulting in a formula with no free variables.

First-order tableau without unification
A first-order formula $$\forall x. \gamma(x)$$ implies all formulae $$\gamma(t)$$ where $$t$$ is a ground term. The following inference rule is therefore correct:

 * $$(\forall) \frac{\forall x . \gamma(x)}{\gamma(t)}$$ where $$t$$ is an arbitrary ground term

Contrarily to the rules for the propositional connectives, multiple applications of this rule to the same formula may be necessary. As an example, the set $$\{\neg P(a) \vee \neg P(b), \forall x. P(x)\}$$ can only be proved unsatisfiable if both $$P(a)$$ and $$P(b)$$ are generated from $$\forall x. P(x)$$.

Existential quantifiers are dealt with by means of Skolemization. In particular, a formula with a leading existential quantifier like $$\exists x. \delta(x)$$ generates its Skolemization $$\delta(c)$$, where $$c$$ is a new constant symbol.

 * $$(\exists) \frac{\exists x . \delta(x)}{\delta(c)}$$ where $$c$$ is a new constant symbol

The Skolem term $$c$$ is a constant (a function of arity 0) because the quantification over $$x$$ does not occur within the scope of any universal quantifier. If the original formula contained some universal quantifiers such that the quantification over $$x$$ was within their scope, these quantifiers have evidently been removed by the application of the rule for universal quantifiers.

The rule for existential quantifiers introduces new constant symbols. These symbols can be used by the rule for universal quantifiers, so that $$\forall y. \gamma(y)$$ can generate $$\gamma(c)$$ even if $$c$$ was not in the original formula but is a Skolem constant created by the rule for existential quantifiers.

The above two rules for universal and existential quantifiers are correct, and so are the propositional rules: if a set of formulae generates a closed tableau, this set is unsatisfiable. Completeness can also be proved: if a set of formulae is unsatisfiable, there exists a closed tableau built from it by these rules. However, actually finding such a closed tableau requires a suitable policy of application of rules. Otherwise, an unsatisfiable set can generate an infinite-growing tableau. As an example, the set $$\{\neg P(f(c)), \forall x. P(x)\}$$ is unsatisfiable, but a closed tableau is never obtained if one unwisely keeps applying the rule for universal quantifiers to $$\forall x. P(x)$$, generating for example $$P(c), P(f(c)), P(f(f(c))), \ldots$$. A closed tableau can always be found by ruling out this and similar "unfair" policies of application of tableau rules.

The rule for universal quantifiers $$(\forall)$$ is the only non-deterministic rule, as it does not specify which term to instantiate with. Moreover, while the other rules need to be applied only once for each formula and each path the formula is in, this one may require multiple applications. Application of this rule can however be restricted by delaying the application of the rule until no other rule is applicable and by restricting the application of the rule to ground terms that already appear in the path of the tableau. The variant of tableaux with unification shown below aims at solving the problem of non-determinism.

First-order tableau with unification
The main problem of tableau without unification is how to choose a ground term $$t$$ for the universal quantifier rule. Indeed, every possible ground term can be used, but clearly most of them might be useless for closing the tableau.

A solution to this problem is to "delay" the choice of the term to the time when the consequent of the rule allows closing at least a branch of the tableau. This can be done by using a variable instead of a term, so that $$\forall x. \gamma(x)$$ generates $$\gamma(x')$$, and then allowing substitutions to later replace $$x'$$ with a term. The rule for universal quantifiers becomes:

 * $$(\forall) \frac{\forall x . \gamma(x)}{\gamma(x')}$$ where $$x'$$ is a variable not occurring everywhere else in the tableau

While the initial set of formulae is supposed not to contain free variables, a formula of the tableau may contain the free variables generated by this rule. These free variables are implicitly considered universally quantified.

This rule employs a variable instead of a ground term. What is gained by this change is that these variables can be then given a value when a branch of the tableau can be closed, solving the problem of generating terms that might be useless.

 * $$(\sigma)$$
 * if $$\sigma$$ is the most general unifier of two literals $$A$$ and $$B$$, where $$A$$ and the negation of $$B$$ occur in the same branch of the tableau, $$\sigma$$ can be applied at the same time to all formulae of the tableau
 * }
 * }

As an example, $$\{\neg P(a), \forall x. P(x)\}$$ can be proved unsatisfiable by first generating $$P(x_1)$$; the negation of this literal is unifiable with $$\neg P(a)$$, the most general unifier being the substitution that replaces $$x_1$$ with $$a$$; applying this substitution results in replacing $$P(x_1)$$ with $$P(a)$$, which closes the tableau. This rule closes at least a branch of the tableau—the one containing the considered pair of literals. However, the substitution has to be applied to the whole tableau, not only on these two literals. This is expressed by saying that the free variables of the tableau are rigid: if an occurrence of a variable is replaced by something else, all other occurrences of the same variable must be replaced in the same way. Formally, the free variables are (implicitly) universally quantified and all formulae of the tableau are within the scope of these quantifiers.

Existential quantifiers are dealt with by Skolemization. Contrary to the tableau without unification, Skolem terms may not be simple constants. Indeed, formulae in a tableau with unification may contain free variables, which are implicitly considered universally quantified. As a result, a formula like $$\exists x. \delta(x)$$ may be within the scope of universal quantifiers; if this is the case, the Skolem term is not a simple constant but a term made of a new function symbol and the free variables of the formula.

 * $$(\exists) \frac{\exists x . \delta(x)}{\delta(f(x_1,\ldots,x_n))}$$ where $$f$$ is a new function symbol and $$x_1,\ldots,x_n$$ the free variables of $$\delta$$

This rule incorporates a simplification over a rule where $$x_1,\ldots,x_n$$ are the free variables of the branch, not of $$\delta$$ alone. This rule can be further simplified by the reuse of a function symbol if it has already been used in a formula that is identical to $$\delta$$ up to variable renaming.

The formula represented by a tableau is obtained in a way that is similar to the propositional case, with the additional assumption that free variables are considered universally quantified. As for the propositional case, formulae in each branch are conjoined and the resulting formulae are disjoined. In addition, all free variables of the resulting formula are universally quantified. All these quantifiers have the whole formula in their scope. In other words, if $$F$$ is the formula obtained by disjoining the conjunction of the formulae in each branch, and $$x_1,\ldots,x_n$$ are the free variables in it, then $$\forall x_1,\ldots,x_n. F$$ is the formula represented by the tableau. The following considerations apply:

 * The assumption that free variables are universally quantified is what makes the application of a most general unifier a sound rule: since $$\gamma(x')$$ means that $$\gamma$$ is true for every possible value of $$x'$$, then $$\gamma(t)$$ is true for the term $$t$$ that the most general unifier replaces $$x$$ with.
 * Free variables in a tableau are rigid: all occurrences of the same variable have to be replaced all with the same term. Every variable can be considered a symbol representing a term that is yet to be decided. This is a consequence of free variables being assumed universally quantified over the whole formula represented by the tableau: if the same variable occurs free in two different nodes, both occurrences are in the scope of the same quantifier. As an example, if the formulae in two nodes are $$A(x)$$ and $$B(x)$$, where $$x$$ is free in both, the formula represented by the tableau is something in the form $$\forall x . (...A(x)...B(x)...)$$. This formula implies that $$(...A(x)...B(x)...)$$ is true for any value of $$x$$, but does not in general imply $$(...A(t)...A(t')...)$$ for two different terms $$t$$ and $$t'$$, as these two terms may in general take different values. This means that $$x$$ cannot be replaced by two different terms in $$A(x)$$ and $$B(x)$$.
 * Free variables in a formula to check for validity are also considered universally quantified. However, these variables cannot be left free when building a tableau, because tableau rules works on the converse of the formula but still treats free variables as universally quantified. For example, $$P(x) \rightarrow P(c)$$ is not valid (it is not true in the model where $$D=\{1,2\}, P(1)=\bot, P(2)=\top, c=1$$, and the interpretation where $$x=2$$). Consequently, $$\{P(x),\neg P(c)\}$$ is satisfiable (it is satisfied by the same model and interpretation). However, a closed tableau could be generated with $$P(x)$$ and $$\neg P(c)$$, and substituting $$x$$ with $$c$$ would generate a closure. A correct procedure is to first make universal quantifiers explicit, thus generating $$\forall x . (P(x) \rightarrow P(c))$$.

The following two variants are also correct.

 * Applying to the whole tableau a substitution to the free variables of the tableau is a correct rule, provided that this substitution is free for the formula representing the tableau. In other worlds, applying such a substitution leads to a tableau whose formula is still a consequence of the input set. Using most general unifiers automatically ensures that the condition of freeness for the tableau is met.
 * While in general every variable has to be replaced with the same term in the whole tableau, there are some special cases in which this is not necessary.

Tableaux with unification can be proved complete: if a set of formulae is unsatisfiable, it has a tableau-with-unification proof. However, actually finding such a proof may be a difficult problem. Contrarily to the case without unification, applying a substitution can modify the existing part of a tableau; while applying a substitution closes at least a branch, it may make other branches impossible to close (even if the set is unsatisfiable).

A solution to this problem is delayed instantiation: no substitution is applied until one that closes all branches at the same time is found. With this variant, a proof for an unsatisfiable set can always be found by a suitable policy of application of the other rules. This method however requires the whole tableau to be kept in memory: the general method closes branches, which can be then discarded, while this variant does not close any branch until the end.

The problem that some tableaux that can be generated are impossible to close even if the set is unsatisfiable is common to other sets of tableau expansion rules: even if some specific sequences of application of these rules allow constructing a closed tableau (if the set is unsatisfiable), some other sequences lead to tableaux that cannot be closed. General solutions for these cases are outlined in the "Searching for a tableau" section.

Tableau calculi and their properties
A tableau calculus is a set of rules that allows building and modification of a tableau. Propositional tableau rules, tableau rules without unification, and tableau rules with unification, are all tableau calculi. Some important properties a tableau calculus may or may not possess are completeness, destructiveness, and proof confluence.

A tableau calculus is called complete if it allows building a tableau proof for every given unsatisfiable set of formulae. The tableau calculi mentioned above can be proved complete.

A remarkable difference between tableau with unification and the other two calculi is that the latter two calculi only modify a tableau by adding new nodes to it, while the former one allows substitutions to modify the existing part of the tableau. More generally, tableau calculi are classed as destructive or non-destructive depending on whether they only add new nodes to tableau or not. Tableau with unification is therefore destructive, while propositional tableau and tableau without unification are non-destructive.

Proof confluence is the property of a tableau calculus being able to obtain a proof for an arbitrary unsatisfiable set from an arbitrary tableau, assuming that this tableau has itself been obtained by applying the rules of the calculus. In other words, in a proof confluent tableau calculus, from an unsatisfiable set one can apply whatever set of rules and still obtain a tableau from which a closed one can be obtained by applying some other rules.

Proof procedures
A tableau calculus is simply a set of rules that prescribes how a tableau can be modified. A proof procedure is a method for actually finding a proof (if one exists). In other words, a tableau calculus is a set of rules, while a proof procedure is a policy of application of these rules. Even if a calculus is complete, not every possible choice of application of rules leads to a proof of an unsatisfiable set. For example, $$\{P(f(c)), R(c), \neg P(f(c)) \vee \neg R(c), \forall x. Q(x)\}$$ is unsatisfiable, but both tableaux with unification and tableaux without unification allow the rule for the universal quantifiers to be applied repeatedly to the last formula, while simply applying the rule for disjunction to the third one would directly lead to closure. For proof procedures, a definition of completeness has been given: a proof procedure is strongly complete if it allows finding a closed tableau for any given unsatisfiable set of formulae. Proof confluence of the underlying calculus is relevant to completeness: proof confluence is the guarantee that a closed tableau can be always generated from an arbitrary partially constructed tableau (if the set is unsatisfiable). Without proof confluence, the application of a 'wrong' rule may result in the impossibility of making the tableau complete by applying other rules.

Propositional tableaux and tableaux without unification have strongly complete proof procedures. In particular, a complete proof procedure is that of applying the rules in a fair way. This is because the only way such calculi cannot generate a closed tableau from an unsatisfiable set is by not applying some applicable rules.

For propositional tableaux, fairness amounts to expanding every formula in every branch. More precisely, for every formula and every branch the formula is in, the rule having the formula as a precondition has been used to expand the branch. A fair proof procedure for propositional tableaux is strongly complete.

For first-order tableaux without unification, the condition of fairness is similar, with the exception that the rule for universal quantifiers might require more than one application. Fairness amounts to expanding every universal quantifier infinitely often. In other words, a fair policy of application of rules cannot keep applying other rules without expanding every universal quantifier in every branch that is still open once in a while.

Searching for a closed tableau
If a tableau calculus is complete, every unsatisfiable set of formulae has an associated closed tableau. While this tableau can always be obtained by applying some of the rules of the calculus, the problem of which rules to apply for a given formula still remains. As a result, completeness does not automatically imply the existence of a feasible policy of application of rules that always leads to a closed tableau for every given unsatisfiable set of formulae. While a fair proof procedure is complete for ground tableau and tableau without unification, this is not the case for tableau with unification.

A general solution for this problem is that of searching the space of tableaux until a closed one is found (if any exists, that is, the set is unsatisfiable). In this approach, one starts with an empty tableau and then recursively applies every possible applicable rule. This procedure visits a (implicit) tree whose nodes are labeled with tableaux, and such that the tableau in a node is obtained from the tableau in its parent by applying one of the valid rules.

Since each branch can be infinite, this tree has to be visited breadth-first rather than depth-first. This requires a large amount of space, as the breadth of the tree can grow exponentially. A method that may visit some nodes more than once but works in polynomial space is to visit in a depth-first manner with iterative deepening: one first visits the tree depth first up to a certain depth, then increases the depth and perform the visit again. This particular procedure uses the depth (which is also the number of tableau rules that have been applied) for deciding when to stop at each step. Various other parameters (such as the size of the tableau labeling a node) have been used instead.

Reducing search
The size of the search tree depends on the number of (children) tableaux that can be generated from a given (parent) one. Reducing the number of such tableaux therefore reduces the required search.

A way for reducing this number is to disallow the generation of some tableaux based on their internal structure. An example is the condition of regularity: if a branch contains a literal, using an expansion rule that generates the same literal is useless because the branch containing two copies of the literals would have the same set of formulae of the original one. This expansion can be disallowed because if a closed tableau exists, it can be found without it. This restriction is structural because it can be checked by looking at the structure of the tableau to expand only. Different methods for reducing search disallow the generation of some tableaux on the ground that a closed tableau can still be found by expanding the other ones. These restrictions are called global. As an example of a global restriction, one may employ a rule that specifies which of the open branches is to be expanded. As a result, if a tableau has for example two non-closed branches, the rule specifies which one is to be expanded, disallowing the expansion of the second one. This restriction reduces the search space because one possible choice is now forbidden; completeness is however not harmed, as the second branch will still be expanded if the first one is eventually closed. As an example, a tableau with root $$\neg a \wedge \neg b$$, child $$a \vee b$$, and two leaves $$a$$ and $$b$$ can be closed in two ways: applying $$(\wedge)$$ first to $$a$$ and then to $$b$$, or vice versa. There is clearly no need to follow both possibilities; one may consider only the case in which $$(\wedge)$$ is first applied to $$a$$ and disregard the case in which it is first applied to $$b$$. This is a global restriction because what allows neglecting this second expansion is the presence of the other tableau, where expansion is applied to $$a$$ first and $$b$$ afterwards.

Clause tableaux
When applied to sets of clauses (rather than of arbitrary formulae), tableaux methods allow for a number of efficiency improvements. A first-order clause is a formula $$\forall x_1,\ldots,x_n L_1 \vee \cdots \vee L_m$$ that does not contain free variables and such that each $$L_i$$ is a literal. The universal quantifiers are often omitted for clarity, so that for example $$P(x,y) \vee Q(f(x))$$ actually means $$\forall x,y. P(x,y) \vee Q(f(x))$$. Note that, if taken literally, these two formulae are not the same as for satisfiability: rather, the satisfiability $$P(x,y) \vee Q(f(x))$$ is the same as that of $$\exists x,y. P(x,y) \vee Q(f(x))$$. That free variables are universally quantified is not a consequence of the definition of first-order satisfiability; it is rather used as an implicit common assumption when dealing with clauses.

The only expansion rules that are applicable to a clause are $$(\forall)$$ and $$(\vee)$$; these two rules can be replaced by their combination without losing completeness. In particular, the following rule corresponds to applying in sequence the rules $$(\forall)$$ and $$(\vee)$$ of the first-order calculus with unification.

 * $$(C) \frac{L_1 \vee \cdots \vee L_n}{L_1'|\cdots|L_n'}$$ where $$L_1' \vee \cdots \vee L_n'$$ is obtained by replacing every variable with a new one in $$L_1 \vee \cdots \vee L_n$$

When the set to be checked for satisfiability is only composed of clauses, this and the unification rules are sufficient to prove unsatisfiability. In other worlds, the tableau calculi composed of $$(C)$$ and $$(\sigma)$$ is complete.

Since the clause expansion rule only generates literals and never new clauses, the clauses to which it can be applied are only clauses of the input set. As a result, the clause expansion rule can be further restricted to the case where the clause is in the input set.

 * $$(C) \frac{L_1 \vee \cdots \vee L_n}{L_1'|\cdots|L_n'}$$ where $$L_1' \vee \cdots \vee L_n'$$ is obtained by replacing every variable with a new one in $$L_1 \vee \cdots \vee L_n$$, which is a clause of the input set

Since this rule directly exploits the clauses in the input set there is no need to initialize the tableau to the chain of the input clauses. The initial tableau can therefore be initialize with the single node labeled $$true$$; this label is often omitted as implicit. As a result of this further simplification, every node of the tableau (apart from the root) is labeled with a literal. A number of optimizations can be used for clause tableau. These optimization are aimed at reducing the number of possible tableaux to be explored when searching for a closed tableau as described in the "Searching for a closed tableau" section above.

Connection tableau
Connection is a condition over tableau that forbids expanding a branch using clauses that are unrelated to the literals that are already in the branch. Connection can be defined in two ways:

 * strong connectedness : when expanding a branch, use an input clause only if it contains a literal that can be unified with the negation of the literal in the current leaf
 * weak connectedness : allow the use of clauses that contain a literal that unifies with the negation of a literal on the branch

Both conditions apply only to branches consisting not only of the root. The second definition allows for the use of a clause containing a literal that unifies with the negation of a literal in the branch, while the first only further constraint that literal to be in leaf of the current branch.

If clause expansion is restricted by connectedness (either strong or weak), its application produces a tableau in which substitution can applied to one of the new leaves, closing its branch. In particular, this is the leaf containing the literal of the clause that unifies with the negation of a literal in the branch (or the negation of the literal in the parent, in case of strong connection).

Both conditions of connectedness lead to a complete first-order calculus: if a set of clauses is unsatisfiable, it has a closed connected (strongly or weakly) tableau. Such a closed tableau can be found by searching in the space of tableaux as explained in the "Searching for a closed tableau" section. During this search, connectedness eliminates some possible choices of expansion, thus reducing search. In other worlds, while the tableau in a node of the tree can be in general expanded in several different ways, connection may allow only few of them, thus reducing the number of resulting tableaux that need to be further expanded.

This can be seen on the following (propositional) example. The tableau made of a chain $$true - a$$ for the set of clauses $$\{a, \neg a \vee b, \neg c \vee d, \neg b\}$$ can be in general expanded using each of the four input clauses, but connection only allows the expansion that uses $$\neg a \vee b$$. This means that the tree of tableaux has four leaves in general but only one if connectedness is imposed. This means that connectedness leaves only one tableau to try to expand, instead of the four ones to consider in general. In spite of this reduction of choices, the completeness theorem implies that a closed tableau can be found if the set is unsatisfiable.

The connectedness conditions, when applied to the propositional (clausal) case, make the resulting calculus non-confluent. As an example, $$\{a, b, \neg b\}$$ is unsatisfiable, but applying $$(C)$$ to $$a$$ generates the chain $$true - a$$, which is not closed and to which no other expansion rule can be applied without violating either strong or weak connectedness. In the case of weak connectedness, confluence holds provided that the clause used for expanding the root is relevant to unsatisfiability, that is, it is contained in a minimally unsatisfiable subset of the set of clauses. Unfortunately, the problem of checking whether a clause meets this condition is itself a hard problem. In spite of non-confluence, a closed tableau can be found using search, as presented in the "Searching for a closed tableau" section above. While search is made necessary, connectedness reduces the possible choices of expansion, thus making search more efficient.

Regular tableaux
A tableau is regular if no literal occurs twice in the same branch. Enforcing this condition allows for a reduction of the possible choices of tableau expansion, as the clauses that would generate a non-regular tableau cannot be expanded.

These disallowed expansion steps are however useless. If $$B$$ is a branch containing a literal $$L$$, and $$C$$ is a clause whose expansion violates regularity, then $$C$$ contains $$L$$. In order to close the tableau, one needs to expand and close, among others, the branch where $$B - L$$, where $$L$$ occurs twice. However, the formulae in this branch are exactly the same as the formulae of $$B$$ alone. As a result, the same expansion steps that close $$B - L$$ also close $$B$$. This means that expanding $$C$$ was unnecessary; moreover, if $$C$$ contained other literals, its expansion generated other leaves that needed to be closed. In the propositional case, the expansion needed to close these leaves are completely useless; in the first-order case, they may only affect the rest of the tableau because of some unifications; these can however be combined to the substitutions used to close the rest of the tableau.

Tableaux for modal logics
In a modal logic, a model comprises a set of possible worlds, each one associated to a truth evaluation; an accessibility relation specifies when a world is accessible from another one. A modal formula may specify not only conditions over a possible world, but also on the ones that are accessible from it. As an example, $$\Box A$$ is true in a world if $$A$$ 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 $$\neg \Box A$$ is true in a world then there exists a world accessible from it where $$A$$ is false. However, one cannot simply add the following rule to the propositional ones.

 * $$\frac{\neg \Box A}{\neg A}$$

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 this into account would generate incorrect results. For example, formula $$a \wedge \neg \Box a$$ states that $$a$$ is true in the current world and $$a$$ is false in a world that is accessible from it. Simply applying $$(\wedge)$$ and the expansion rule above would produce $$a$$ and $$\neg a$$, 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 $$M$$ and world $$w$$ such that the formulae in the set are true in that model and world. In the example above, while $$a$$ states the truth of $$a$$ in $$w$$, the formula $$\neg \Box a$$ states the truth of $$\neg a$$ in some world $$w'$$ that is accessible from $$w$$ and which may in general be different from $$w$$. 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 $$\neg \Box A \wedge \neg \Box B$$ is true if a successor where $$\neg A$$ holds exists and a successor where $$\neg B$$ holds exists. In the other way around, if one can show unsatisfiability of $$\neg A$$ in an arbitrary successor, the formula is proved unsatisfiable without checking for worlds where $$\neg B$$ holds. At the same time, if one can show unsatisfiability of $$\neg B$$, there is no need to check $$\neg A$$. As a result, while there are two possible way to expand $$\neg \Box A \wedge \neg \Box B$$, one of these two ways is always sufficient to prove unsatisfiability if the formula is unsatisfiable. For example, one may expand the tableau by considering an arbitrary world where $$\neg A$$ holds. If this expansion leads to unsatisfiability, the original formula is unsatisfiable. However, it is also possible that unsatisfiability cannot be proved this way, and that the world where $$\neg B$$ holds should have been considered instead. As a result, one can always prove unsatisfiability by expanding either $$\neg \Box A$$ only or $$\neg \Box B$$ only; however, if the wrong choice is made the resulting tableau may not be closed. Expanding either subformula leads to tableau calculi that are complete but not proof-confluent. Searching as described in the "Searching for a closed tableau" may therefore be necessary.

Depending on whether the precondition and consequence of a tableau expansion rule refer to the same world or not, the rule is called static or transactional. While rules for propositional connectives are all static, not all rules for modal connectives are transactional: for example, in every modal logic including axiom T, it holds that $$\Box A$$ implies $$A$$ in the same world. As a result, the relative (modal) tableau expansion rule is static, as both its precondition and consequence refer to the same world.

Formula-deleting tableau
A method for avoiding formulae referring to different worlds interacting in the wrong way is to make sure that all formulae of a branch refer to the same world. This condition is initially true as all formulae in the set to be checked for consistency are assumed referring to the same world. When expanding a branch, two situations are possible: either the new formulae refer to the same world as the other one in the branch or not. In the first case, the rule is applied normally. In the second case, all formulae of the branch that do not also hold in the new world are deleted from the branch, and possibly added to all other branches that are still relative to the old world.

As an example, in S5 every formula $$\Box A$$ that is true in a world is also true in all accessible worlds (that is, in all accessible worlds both $$A$$ and $$\Box A$$ are true). Therefore, when applying $$\frac{\neg \Box B}{\neg B}$$, whose consequence holds in a different world, one deletes all formulae from the branch, but can keep all formulae $$\Box A$$, 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 $$A$$, one would write $$w:A$$ to make it explicit that $$A$$ holds in world $$w$$.

All propositional expansion rules are adapted to this variant by stating that they all refer to formulae with the same world label. For example, $$w:A \wedge B$$ generates two nodes labeled with $$w:A$$ and $$w:B$$; a branch is closed only if it contains two opposite literals of the same world, like $$w:a$$ and $$w:\neg a$$; no closure is generated if the two world labels are different, like in $$w:a$$ and $$w':\neg a$$.

A modal expansion rule may have a consequence that refers to different worlds. For example, the rule for $$\neg \Box A$$ would be written as follows

 * $$\frac{w:\neg \Box A}{w':\neg A}$$

The precondition and consequent of this rule refer to worlds $$w$$ and $$w'$$, respectively. The various calculi use different methods for keeping track of the accessibility of the worlds used as labels. Some include pseudo-formulae like $$wRw'$$ to denote that $$w'$$ is accessible from $$w$$. Some others use sequences of integers as world labels, this notation implicitly representing the accessibility relation (for example, $$(1,4,2,3)$$ is accessible from $$(1,4,2)$$.)

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 $$S$$, they check the existence of a model $$M$$ and a world $$w$$ such that $$M,w \models S$$.

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:

 * $$(K) \frac{\Box A_1; \ldots ; \Box A_n ; \neg \Box B}{A_1; \ldots ; A_n ; \neg B}$$

Intuitively, the precondition of this rule expresses the truth of all formulae $$A_1,\ldots,A_n$$ at all accessible worlds, and truth of $$\neg B$$ at some accessible worlds. The consequence of this rule is a formula that must be true at one of those worlds where $$\neg B$$ is true.

More technically, modal tableaux methods check the existence of a model $$M$$ and a world $$w$$ that make set of formulae true. If $$\Box A_1; \ldots ; \Box A_n ; \neg \Box B$$ are true in $$w$$, there must be a world $$w'$$ that is accessible from $$w$$ and that makes $$A_1; \ldots ; A_n ; \neg B$$ true. This rule therefore amounts to deriving a set of formulae that must be satisfied in such $$w'$$.

While the preconditions $$\Box A_1; \ldots ; \Box A_n ; \neg \Box B$$ are assumed satisfied by $$M,w$$, the consequences $$A_1; \ldots ; A_n ; \neg B$$ are assumed satisfied in $$M,w'$$: 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, $$(K)$$ does not directly extend to multiple negated boxed formulae such as in $$\Box A_1; \ldots; \Box A_n; \neg \Box B_1; \neg \Box B_2$$: while there exists an accessible world where $$B_1$$ is false and one in which $$B_2$$ is false, these two worlds are not necessarily the same.

Differently from the propositional rules, $$(K)$$ states conditions over all its preconditions. For example, it cannot be applied to a node labeled by $$a; \Box b; \Box (b \rightarrow c); \neg \Box c$$; while this set is inconsistent and this could be easily proved by applying $$(K)$$, this rule cannot be applied because of formula $$a$$, which is not even relevant to inconsistency. Removal of such formulae is made possible by the rule:

 * $$(\theta) \frac{A_1;\ldots;A_n;B_1;\ldots;B_m}{A_1;\ldots;A_n}$$

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 $$(\theta)$$ 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 $$(\theta)$$ so 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 $$(\theta)$$ 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:

 * $$(T) \frac{A_1;\ldots;A_n;\Box B}{A_1;\ldots;A_n; \Box B; B}$$

This rule relates conditions over the same world: if $$\Box B$$ is true in a world, by reflexivity $$B$$ 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 $$\Box B$$ from the precondition to the consequent, in spite of this formula having been "used" to generate $$B$$. This is correct, as the considered world is the same, so $$\Box B$$ also holds there. This "copying" is necessary in some cases. It is for example necessary to prove the inconsistency of $$\Box(a \wedge \neg \Box a)$$: the only applicable rules are in order $$(T), (\wedge), (\theta), (K)$$, from which one is blocked if $$\Box a$$ 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, $$\neg \Box A$$ implies that $$A$$ is false in an accessible world, so one starts a new tableau rooted by $$\neg A$$. 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 $$M$$, if $$A$$ is true in a world $$w$$, then $$B$$ is also true in the same world. This is the same as checking whether $$B$$ is true in a world of a model, in the assumption that $$A$$ is also true in the same world of the same model.

A related problem is the global consequence problem, where the assumption is that a formula (or set of formulae) $$G$$ is true in all possible worlds of the model. The problem is that of checking whether, in all models $$M$$ where $$G$$ is true in all worlds, $$B$$ 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, $$\{P, \neg \Box (P \wedge Q)\}$$ entails $$\neg \Box Q$$ globally but not locally. Local entailment does not hold in a model consisting of two worlds making $$P$$ and $$\neg P, Q$$ true, respectively, and where the second is accessible from the first; in the first world, the assumptions are true but $$\neg \Box Q$$ is false. This counterexample works because $$P$$ can be assumed true in a world and false in another one. If however the same assumption is considered global, $$\neg P$$ is not allowed in any world of the model.

These two problems can be combined, so that one can check whether $$B$$ is a local consequence of $$A$$ under the global assumption $$G$$. 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 $$\alpha$$ is always considered to be $$\alpha_1 \wedge \alpha_2$$. 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 $$\overline{\alpha_1}$$ indicates that $$\alpha_1$$ is the negation of whatever formula appears in its place, so that for example in formula $$\neg (a \vee b)$$ the subformula $$\alpha_1$$ is the negation of $$a$$.

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:

 * $$(\alpha) \frac{\alpha}{\begin{array}{c}\alpha_1\\ \alpha_2\end{array}}$$

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.

title: Method of analytic tableaux


text:
Sherone Simpson

Sherone Simpson (born 12 August 1984) is a Jamaican retired track and field sprint athlete. She is a gold medalist in the 4 × 100 m relay from the 2004 Olympics and silver medalist in 2005 World Championships and now is the silver medalist in the individual event at the 2008 Summer Olympics, after she tied for second with Kerron Stewart in a photo finish.

On 14 July 2013, Simpson announced that she had tested positive for the drug oxilofrine. In April 2014, the Jamaica Anti-Doping Commission announced that she would be suspended for 18 months over doping charges, expiring in December that year. However, after appealing to the Court of Arbitration for Sport (CAS), the suspension was lifted on 14 July 2014.

Biography
With her personal best of 10.82 seconds in the 100 m, Simpson is ranked 7th among Jamaican women, behind Elaine Thompson-Herah (10.54), Shelly-Ann Fraser-Pryce (10.60), Shericka Jackson (10.65), Merlene Ottey (10.74), Kerron Stewart (10.75), and Veronica Campbell Brown (10.76). Simpson's 200 m personal best of 22.00 seconds ranks her 9th among Jamaican women behind Elaine Thompson-Herah, Merlene Ottey, Grace Jackson, Veronica Campbell-Brown, Juliet Cuthbert, Shelly-Ann Fraser-Pryce, Shericka Jackson and Kerron Stewart. She has run this time on two occasions. Simpson is coached by Stephen Francis in Kingston, Jamaica, where she attends the University of Technology. She is also a graduate of Manchester High.

Simpson won the gold medal in the women's 200 m at the 2006 Commonwealth Games, beating Olympic champion Veronica Campbell and completing a Jamaican sweep of 100–200 m gold medals. Jamaica also won both sprint hurdles gold medals.

At the 2008 Summer Olympics in Beijing she competed at the 100 m sprint. In her first round heat she placed third behind Yevgeniya Polyakova and Jade Bailey in a time of 11.48 to advance to the second round. There she improved her time to 11.02 seconds to win her heat in front of Muna Lee and Chandra Sturrup. With 11.11 seconds in her semi final race she placed fourth and earned her spot in the Olympic final. In a remarkable race with fellow Jamaican Shelly-Ann Fraser taking the gold, Simpson and Kerron Stewart both finished in 10.98 seconds to share the silver medal and to complete the Jamaican sweep. Together with Fraser, Stewart, Sheri-Ann Brooks, Aleen Bailey and Veronica Campbell-Brown she also took part in the 4 × 100 m relay. In their first round heat (without Simpson and Stewart) they placed first in front of Russia, Germany and China. Their time of 42.24 seconds was the first time overall out of sixteen participating nations. With this result they qualified for the final, in which they replaced Brooks and Bailey with Simpson and Stewart. Eventually they did not finish their race, due to a mistake in the baton exchange.

Brief suspension
On 14 July 2013, Simpson informed that a urine sample she supplied after competing in the Jamaican national championships in June 2013 had tested positive for the banned stimulant oxilofrine, along with Asafa Powell. On 10 April 2014, both athletes received an 18-month suspension from competing, which was set to expire in December that year. However, after appealing to the Court of Arbitration for Sport (CAS), both athletes' suspensions were lifted on 14 July 2014. CAS stated that: "They put forward that the offence committed was minor because it was caused by contamination of the food supplement Epiphany D1 by the banned substance oxilofrine and requested that the suspensions be reduced to three months."

license: Creative Commons - Attribution Share-Alike - https://creativecommons.org/licenses/by-sa/4.0/

title: Sherone Simpson


text:
Lokaksema (Buddhist monk)

Lokakṣema (लोकक्षेम, ) (flourished 147–189) was a Kushan Buddhist monk from Gandhara who traveled to China during the Han dynasty and translated Buddhist texts into Chinese, and, as such, is an important figure in Chinese Buddhism.

Biography
Details of Lokakṣema's life come to us via a short biography by Sengyou (僧祐; pinyin: Sēngyòu; 445–518 CE) and his text "Collected Records concerning the Tripitaka" (出三藏記集 Chu sanzang jìjí, T2145).

The name 婁迦讖 is usually rendered in Sanskrit as Lokakṣema, though this is disputed by some scholars, and variants such as Lokakṣama have been proposed. In particular the character 讖 can be read as chen or chan. Sengyou refers to him as Zhīchèn. The Zhī prefix added to his Chinese name suggests that Lokaksema was of Yuezhi  ethnicity. He is traditionally said to have been a Kushan, though the Chinese term Yuezhi covered a broad area of what is now Iran, Afghanistan, and Pakistan.

Lokaksema was born in Gandhara, a center of Greco-Buddhist art, at a time when Buddhism was actively sponsored by the king, Kanishka the Great, who convened the Fourth Buddhist council. The proceedings of this council actually oversaw the formal split of Nikaya and Mahayana Buddhism. It would seem that Kanishka was not ill-disposed towards Mahayana Buddhism, opening the way for missionary activities in China by monks such as Lokakṣema.

Lokaksema arrived in the Han capital Luoyang toward the end of the reign of Emperor Huan of Han (r.147-168), and between 178 and 189 CE translated a number of Mahayāna Buddhist texts into Chinese.

Lokaksema's translation activities, as well as those of the Parthians An Shigao and An Xuan slightly earlier, or his fellow Yuezhi Dharmarakṣa (around 286 CE) illustrate the key role Central Asians had in propagating Buddhism to the countries of East Asia. With the decline and fall of the Han, the empire fell into chaos and Lokakṣema disappears from the historical record so that we do not know the date of his death.

Extant translations
The editors of the Taishō Tripiṭaka attribute twelve texts to Lokakṣema. These attributions have been studied in detail by Erik Zürcher, Paul Harrison and Jan Nattier, and some have been called into question.

Zürcher considers it reasonably certain that Lokakṣema translated the following:

 * T224. 道行般若經. A translation of the Aṣṭasāhasrikā Prajñāpāramitā Sūtra.
 * T280. 佛說兜沙經. The Scripture on the Tusita Heaven, part of the proto-Avatamsaka Sutra
 * T313. 阿閦佛國經. Akṣohhya-vyūha
 * T350. 說遺日摩尼寶經. Kaśyapaparivrata
 * T418. 般舟三昧經. Pratyutpanna Samādhi Sūtra
 * T458. 文殊師利問菩薩署經. Mañjuśrī's Inquiry Concerning the Bodhisattva Career.
 * T626. 阿闍世王經. Ajātaśatru Kaukṛtya Vinodana Sūtra
 * T807. 佛說內藏百寶經. The Hundred Jewels of the Inner Treasury.

According to Nattier, Harrison "expresses reservations" concerning the Akṣohhya-vyūha (T313), and considers that T418 is the product of revision and does not date from Lokakṣema's time.

Conversely, Harrison considers that the following ought to be considered genuine:

 * T624 伅真陀羅所問如來三昧經 Druma-kinnara-rāja-paripṛcchā-sūtra

A characteristic of Lokakṣema's translation style was the extensive transliteration of Indic terms and his retention of India stylistic features such as long sentences. He typically rendered Indic verse as Chinese prose, making no attempt to capture the meter. Based on evidence from Chinese catalogues of texts, Nattier suggests that T224 and T418 are representative of Lokakṣema and might stand as "core texts", i.e. as representative of his style of translating, although both show some signs of later editing. A second tier of texts—T280, T350, T458, and T807—all strongly resemble Lokakṣema's core texts, though with occasional anomalies. T624 and T626 form a third tier with more deviations from the distinctive style of Lokakṣema. If T313 was indeed a translation by Lokakṣema, it has been extensively revised by an unknown editor, though the prose sections are closer to his style than the verse.

Lost works
Several translations attributed to Lokakṣema have been lost:

 * Shoulengyan jing (a version of the Suramgama-samādhi-siitra, already lost in Sengyou's time)
 * Guangming sanmei jing "Sutra on the Samadhi of Luminosity"
 * Hu banniehuan jing "The Hu Parinirvāṇa Sutra"
 * Bo benjing ("The Original *Puṣya Sutra")

title: Lokaksema (Buddhist monk)


text:
Tayna Lawrence

Tayna Lawrence (born 17 September 1975 in Spanish Town, Jamaica) is a retired Track and field sprint athlete who competed internationally for Jamaica. She is an Olympic gold medalist in the 4 x 100 meter relay race.

Lawrence graduated from Florida International University, in Miami, Florida, USA. She sustained a leg injury and had to undergo surgery in 2003, missing the World Championships in Paris. She was severely hampered by a series of stress fractures in 2001, which ruled her out of the World Championships.

Personal bests
* Marion Jones, the American athlete who finished in first place, was stripped of her gold medal in October 2007 following a doping scandal. Ekaterini Thanou, the Greek athlete who finished second place, was later suspended for two years following various scandals at the 2004 Summer Olympics.

Videos

 * Flotrack Videos of Tayna Lawrence

title: Tayna Lawrence


text:
Biryani

Biryani is a mixed rice dish from Iran its mainly popular in South Asia & Iran. It is made with rice, some type of meat (chicken, goat, pork, lamb, beef, prawn, or fish) and spices. To cater to vegetarians, in some cases, it is prepared by substituting vegetables or paneer for the meat. Sometimes eggs and/or potatoes are also added.

Biryani is one of the most popular dishes in South Asia and among the South Asian diaspora, although the dish is often associated with the region's Muslim population in particular. Similar dishes are also prepared in other parts of the world such as in Iraq, Myanmar, Thailand, and Malaysia. Biryani is the single most-ordered dish on Indian online food ordering and delivery services, and has been labelled as the most popular dish overall in India.

Etymology
One theory states that it originated from birinj, the Persian word for rice. Another theory states that it is derived from biryan or beriyan, which means "to fry" or "to roast". It may alternatively be related to the Persian word bereshtan which also means "to roast (onions)", as the dish is often prepared by flavouring rice with fried onions and meat, besides mild spices.

North India
The exact origin of the dish is uncertain, however, it is speculated to have originated in Iran. In North India, different varieties of biryani developed.

According to historian Lizzie Collingham, the modern biryani developed in the royal kitchens of the Mughal Empire (1526–1857) and is a mix of the native spicy rice dishes of India and the Persian polao. Indian restaurateur Kris Dhillon believes that the dish originated in Persia and was brought to India by the Mughals. Salma Hossein, whom the BBC regards as the "doyenne of Islamic cooking in India", shares a similar view, asserting that biryani came to India from Persia even before the Mughal era. Food scholar Pushpesh Pant also challenges the Mughal-origin claim, stating that it originated in Iran and that "there is no evidence that biryani first came to this land with the Moguls. It is far more probable that it travelled with pilgrims and soldier-statesmen of noble descent to the Deccan region in South India".

Another theory claims that the dish was prepared in India before the first Mughal emperor Babur conquered India. The 16th-century Mughal text Ain-i-Akbari makes no distinction between biryanis and pilaf (or pulao): it states that the word "biryani" is of older usage in India. A similar theory, that biryani came to India with Timur's invasion, appears to be incorrect because there is no record of biryani having existed in his native land during that period.

According to Pratibha Karan, who wrote the book Biryani, biryani is of Mughal origin, derived from pilaf varieties brought to the Indian subcontinent by Arab traders. She speculates that the pulao was an army dish in medieval India. Armies would prepare a one-pot dish of rice with whichever meat was available. Over time, the dish became biryani due to different methods of cooking, with the distinction between "pulao" and "biryani" being arbitrary.

According to Vishwanath Shenoy, the owner of a biryani restaurant chain in India, one branch of biryani comes from the Mughals, while another was brought by the Arab traders to Malabar in South India.

There are various apocryphal stories dating the invention to Shah Jahan's time but Rana Safvi, the distinguished historian, says she could only find a recipe from the later Mughal period, from Bahadur Shah Zafar's time. It is not her claim that there was no biryani before that; just that she has not found a recipe. Other historians who have gone through texts say that the first references to biryani only appear around the 18th century.

South India
Some claim that the dish "oonchoru" as mentioned in Sangam literature, which dates from between 200 BCE and 200 CE, is a predecessor of modern biryani. This dish, which was served to the soldiers of the Chera kings in Kerala, was said to be made of rice, ghee, meat, turmeric, coriander, pepper, and bay leaf.

The spices utilized in the preparation of South Indian biryanis, such as those used in the Malabar variety, are distinctive to the region and the Western Ghats. These spices are not found in the Middle East, Persia, or North India, underscoring the unique culinary heritage and local ingredients of South Indian biryani.

In South India, where rice is more widely used as a staple food, several distinct varieties of biryani emerged from Hyderabad in Telangana, Vijayawada in Andhra Pradesh, Mangalore and Bhatkal in Coastal Karnataka, Thalassery and Kozhikode in Malabar Kerala, as well as Ambur and Chettinad in Tamil Nadu.

Difference between biryani and pulao
Pilaf or pulao, as it is known on the Indian subcontinent, is another mixed rice dish popular in the cuisines of the Indian subcontinent, Central Asia, and Middle Eastern cuisine. Opinions differ on the differences between pulao and biryani, and whether actually there is a difference between the two.

According to Delhi-based historian Sohail Hashmi, pulao tends to be plainer than biryani, and consists of meat or vegetables cooked with rice with the bottom layered with potatoes or onions. Biryani contains more gravy (or yakhni), and is often cooked longer, leaving the meat (and vegetables, if present) more tender, and the rice more flavoured. Biryani is also cooked with additional dressings and often would have a light layer of scorched rice at the bottom.

Author Pratibha Karan states that while the terms are often applied arbitrarily, the main distinction is that a biryani consists of two layers of rice with a layer of meat (and vegetables, if present) in the middle, while the pulao is not layered.

Author Colleen Taylor Sen lists the following distinctions between biryani and pulao:
 * Biryani is the primary dish in a meal, while the pulao is usually a secondary accompaniment to a larger meal.
 * In biryani, meat (and vegetables, if present) and rice are cooked separately before being layered and cooked together for the gravy to absorb into the rice. Pulao is a single-pot dish: meat (or vegetables) and rice are cooked separately and they are not mixed. However, some other writers have reported pulao recipes in which the rice and meat are cooked together and then simmered for dum cooking until the liquid is absorbed.
 * Biryanis have more complex and stronger spices compared to pulao.
 * The British-era author Abdul Halim Sharar mentions that biryani has a stronger taste of curried rice due to a greater amount of spices.

Ingredients
Ingredients for biryani vary according to the region and the type of meat and vegetables used. Meat (chicken, goat, beef, lamb, prawn or fish) is the prime ingredient with rice. As is common in dishes of the Indian subcontinent, vegetables are sometimes also used when preparing biryani. Corn may be used depending on the season and availability. Navratan biryani tends to use sweeter, richer ingredients such as cashews, sultanas (kismis), and fruits such as apples and pineapples.

The spices and condiments used in biryani may include fennel seeds, ghee (clarified butter), nutmeg, mace, pepper, cloves, cardamom, cinnamon, bay leaves, coriander, mint, ginger, onions, tomatoes, green chilies, star anise, and garlic. The premium varieties include saffron. Some commercial recipes for Biryani also include aromatic essences such as Mitha Ittar see attar, kewra and rose water. Dried sour prunes (Alu Bukhara) may also be added to the biryani. In nasi briyani and other variants made in Southeast Asian countries such as Malaysia, Singapore, and Indonesia, typical Southeast Asian spices and aromatics such as pandan leaf may be used alongside typical South Asian spices.

The main ingredient that usually accompanies the spices is chicken, lamb or goat meat; special varieties might use beef or seafood instead. The dish may be served with dahi chutney or raita, seekh kebab, korma, curry, a sour dish of aubergine (brinjal), boiled egg, and salad.

Preparation styles
Biryani can be cooked using one of two styles/techniques, pakki ("cooked") and kacchi ("raw").
 * In a pakki biryani, the rice, marinated meat, and any vegetables are partially ("three-quarters") cooked separately, before being combined into layers in a cooking vessel. Different layers of rice may be treated with different spices (e.g., with dissolved saffron or turmeric to give the rice different colours and flavours). The contents are then baked to complete the cooking and allow the flavours to combine. Alternatively, the components may be fully cooked, and then simply combined by layering before serving.
 * In a kacchi biryani, layers of raw marinated meat are alternated in layers with wet, pre-soaked, raw rice (which may be treated with different spices as above), and cooked together by baking, or medium-to-low direct heat (typically, for at least an hour). Cooking occurs by a process of steaming from the ingredients' own moisture: the cooking vessel's lid is sealed (traditionally, with a strip of wheat dough) so that steam cannot escape (proper dum pukht).
 * A yoghurt-based marinade at the bottom of the cooking pot provides additional flavour and moisture. Potatoes often comprise the bottom layer (a technique also used in Iranian cuisine), because, with their natural moisture content, they brown well with less risk of getting burned accidentally. The lid is not opened until the dish is ready to serve. Kacchi biryani is technically much more demanding and time-consuming than pakki biryani, for the following reasons:
 * The different ingredients—meat, rice, potatoes—have different cooking times: tender cuts of meat/chicken can be fully cooked well before the rice is done. To prevent this, many kacchi recipes use parboiled (semi-cooked) rice rather than raw rice.
 * If direct heat is used, there is a risk that the food layer in contact with the vessel bottom may get burned while the interior's contents are still raw. This risk is minimized by sustained baking with moderate heat or very slow cooking on low direct heat. This approach, however, increases cooking time considerably.
 * One method is cooking the dish "blind", with the cooking vessel sealed, so one cannot monitor the cooking progress—it takes the understanding of the raw foods used, the heat required to cook those raw foods, and how the climate can affect the cooking process. Hence making kacchi biryani requires a seasoned hand.

On the Indian subcontinent
There are many types of biryani, whose names are often based on their region of origin. For example, Sindhi biryani developed in the Sindh region of what is now Pakistan, and Hyderabadi biryani developed in the city of Hyderabad in South India.

Some have taken the name of the shop that sells it, for example: Haji Biriyani, Haji Nanna Biriyani in Old Dhaka, Fakhruddin Biriyani in Dhaka, Students biryani in Karachi, Lucky biryani in Bandra, Mumbai and Baghdadi biryani in Colaba, Mumbai. Biryanis are often specific to the Muslim communities where they originate; they are usually the defining dishes of those communities.

Ambur/Vaniyambadi biryani
Ambur/Vaniyambadi biryani is a variety cooked in the neighboring towns of Ambur and Vaniyambadi in the Tirupattur district of the northeastern part of Tamil Nadu, which has a high Muslim population. It was introduced by the Nawabs of Arcot who once ruled the area. It is typically made with jeera samba rice.

The Ambur/Vaniyambadi biryani is accompanied by dhalcha, a sour brinjal curry, and pachadi or raitha (sliced onions mixed with plain yogurt, tomato, chilies, and salt). It has a distinctive aroma and is considered light on the stomach. The usage of spice is moderate and curd is used as a gravy base. It also has a higher ratio of meat to rice. Ambur-style biriyani is popular as street food all across South India.

Beef/Kalyani biryani
Beef biryani, as the name implies, uses beef as the meat. In Hyderabad, it is famous as Kalyani biryani, in which buffalo or cow meat is used. This meal was started after the Kalyani Nawabs of Bidar came to Hyderabad sometime in the 18th century. The Kalyani biryani is made with small cubes of beef, regular spices, onions, and many tomatoes. It has a distinct tomato, jeera and dhania flavour. In Kerala, beef biryani is well known.

Bhatkali/Navayathi biryani
This is an integral part of the Navayath cuisine and a specialty of Bhatkal, a coastal town in Karnataka. Its origins are traced to the Persian traders who left behind not only biryani but a variation of kababs and Indian breads. In Bhatkali biryani, the meat is cooked in an onion and green chili-based masala and layered with fragrant rice. It has a unique spicy and heady flavour, and the rice is overwhelmingly white with mild streaks of orange. Its variations include beef, goat, chicken, titar (Partridge), egg, fish, crab, prawn, and vegetable biryani.

Though similar to those in Thalassery, this biryani differs with lingering after-notes of mashed onions laced with garlic. A few chilies and spices littered with curry leaves lends a unique flavour to Bhatkal biryani. No oil is used.

Bohri biryani
Bohri biryani, prepared by the Bohris is flavoured with lots of tomatoes. It is popular in Karachi.

Chettinad biryani
Chettinad biryani is famous in the Indian state of Tamil Nadu. It is made of jeeraka samba rice, and smells of spices and ghee. It is best taken with nenju elumbu kuzhambu, a spicy and tangy goat meat gravy. The podi kozhi is usually topped with fried onions and curry leaves.

Degh ki biryani/akhni biryani of Parbhani
Degh ki biryani is a typical biryani made from small cubes of beef or mutton. This biryani is famous in Parbhani and generally served at weddings.

The meat is flavoured with ginger, garlic, red chili, cumin, garam masala, fried onion and curd. This biryani is also known as kachay gosht ki biryani or dum biryani, where the meat is marinated and cooked along with short-grained and fine rice. It is left on a slow fire or dum for a fragrant and aromatic flavour.

Delhi biryani
The Delhi version of biryani developed a unique local flavour as the Mughal kings shifted their political capital to the North Indian city of Delhi. Until the 1950s, most people cooked biryani in their home and rarely ate at eateries outside of their homes. Hence, restaurants primarily catered to travellers and merchants. Any region that saw more of these two classes of people nurtured more restaurants, and thus their own versions of biryani. This is the reason why most shops that sold biryani in Delhi, tended to be near mosques such as Jama Masjid (for travellers) or traditional shopping districts (such as Chandni Chowk).

Each part of Delhi has its own style of biryani, often based on its original purpose, thus giving rise to Nizamuddin biryani, Shahjahanabad biryani, etc. Nizamuddin biryani usually had little expensive meat and spices as it was primarily meant to be made in bulk for offering at the Nizamuddin Dargah shrine and thereafter to be distributed to devotees. A non-dum biryani, using many green chillies, popularized by the Babu Shahi Bawarchi shops located outside the National Sports Club in Delhi is informally called Babu Shahi biryani. Another version of Delhi biryani uses achaar (pickles) and is called achaari biryani.

Dhakaiya biryani
The city of Dhaka in Bangladesh is known for selling Chevon Biryani, a dish made with highly seasoned rice and goat meat. The recipe includes: highly seasoned rice, goat meat, mustard oil, garlic, onion, black pepper, saffron, clove, cardamom, cinnamon, salt, lemon, doi, peanuts, cream, raisins and a small amount of cheese (either from cows or buffalo). Haji biryani is a favourite among Bangladeshis living abroad. A recipe was handed down by the founder of one Dhaka restaurant to the next generation. Haji Mohammad Shahed claimed, "I have never changed anything, not even the amount of salt". Bengali style biryani often includes potatoes.

Dhakaiya Kacchi Biryani is accompanied by borhani, a salted mint drink made of yogurt, coriander, mint and salt.

Dindigul biryani
The city of Dindigul in Tamil Nadu is noted for its biryani, which uses a little curd and lemon juice for a tangy taste.

Donne biryani
Military hotels of Bangalore in Karnataka are known for selling Biryani served in dried plantain leaf bowl called Donne. It is typically made from jeera samba rice, yogurt with lot of common mint and coriander leaves.

Hyderabadi biryani
Hyderabadi biryani is India's most famous biryani; some say biryani is synonymous with Hyderabad. Hyderabadi biryani developed under the rule of Asaf Jah I, who was first appointed as the governor of Deccan by the Mughal Emperor Aurangzeb. It is made with basmati rice, spices and goat meat. Popular variations use chicken instead of goat meat. There are various forms of Hyderabadi biryani, such as kachay gosht ki biryani or dum biryani, where goat meat is marinated and cooked along with the rice. It is left on a slow fire or dum for a fragrant and aromatic flavour.

Memoni/Kutchi biryani
Memoni biryani is an extremely spicy variety developed by the Memons of Gujarat-Sindh region in India and Pakistan. It is made with mutton, dahi, fried onions, and potatoes, and fewer tomatoes compared to Sindhi biryani.

Kalyani biryani
Kalyani biryani is a typical biryani from the former state of Hyderabad Deccan. Also known as the "poor man's" Hyderabadi biryani, Kalyani biryani is always made from small cubes of buffalo meat.

The meat is flavoured with ginger, garlic, turmeric, red chili, cumin, coriander powder, and much onion and tomato. It is first cooked as a thick curry and then cooked along with rice. Then given dum (the Indian method of steaming in a covered pot).

Kalyani biryani is supposed to have originated in Bidar during the reign of the Kalyani Nawabs, who migrated to Hyderabad after one of the Nawabs, Ghazanfur Jang married into the Asaf Jahi family uniting their realms. Kalyani biryani was served by the Kalyani Nawabs to all of their subjects who came from Bidar to Hyderabad and stayed or visited their devdi or noble mansion.

Kolkata biryani
Calcutta or Kolkata biryani evolved from the Lucknow style when Awadh's last Nawab, Wajid Ali Shah, was exiled in 1856 to the Kolkata suburb of Metiabruz. Shah brought his personal chef with him. The Kolkata biriyani is characterized by the presence of potato in it.

Mangalore / Beary Biryani
A specialty of the Beary Muslim community in coastal Karnataka and is also known as Manglorean-style biryani. The dish is made using lots of green chilly and coconut and has the subtle flavor and aroma of fennel. Spices that include nutmeg, mint leaves, fennel seeds, mace (javitri), poppy seeds, almonds, star anise and others. The rice and meat (mutton, chicken, beef) are cooked separately and then layered and slowly cooked together again. This dish is highly served during marriages and other homely occasions.

Rawther biryani
This type of biryani is popular in the Palakkad and Coimbatore regions. This was most commonly prepared by Rawther families in Kerala and Tamil Nadu. This type of biryani is cooked in a different style. Goat meat is most commonly used and it is entirely different from Malabar biryani.

Sindhi biryani
The exotic and aromatic Sindhi biryani is known in Pakistan for its spicy taste, fragrant rice, and delicate meat. Sindhi biryani is a beloved staple in food menus of Pakistani and Sindhi cuisine. Sindhi biryani is prepared with meat and a mixture of basmati rice, vegetables, and various spices.

Sri Lankan biryani
Biryani was brought into Sri Lanka by the South Indian Muslims who were trading in the Northern part of Sri Lanka and in Colombo in the early 1900s. In Sri Lanka, it is Buryani, a colloquial word which generated from Buhari Biryani. In many cases, Sri Lankan biryani is much spicier than most Indian varieties. Side dishes may include acchar, Malay pickle, cashew curry and mint sambol.

Thalassery biryani
Thalassery biryani is the variation of biryani found in the Indian state of Kerala. It is one of the many dishes of the Kerala Muslim community, and very popular.

The ingredients are chicken, spices and the specialty is the choice of rice called khyma. Khyma rice is generally mixed with ghee. Although a large number of spices such as mace, cashew nuts, sultana raisins, fennel-cumin seeds, tomato, onion, ginger, garlic, shallot, cloves and cinnamon are used, there is only a small amount of chili (or chili powder) used in its preparation.

A pakki biryani, the Thalassery biryani uses a small-grained thin (not round) fragrant variety of rice known as khyma or jeerakasala. The dum method of preparation (sealing the lid with dough [maida] or cloth and placing red-hot charcoal above the lid) is applied here to avoid scorched rice.

Burma

In Myanmar (Burma), biryani is known in Burmese as danpauk or danbauk, derived from the Persian term dum pukht, which refers to a slow oven cooking technique. Danbauk is a mainstay at festive events such as Thingyan, weddings and donation feasts. Given danbauk 's South Asian origins, danbauk restaurants and chains have traditionally been owned by Muslims, but in recent decades Buddhist entrepreneurs have entered the market.

Featured ingredients include: cashew nuts, yogurt, raisins and peas, chicken, cloves, cinnamon, saffron and bay leaf cooked in long-grain rice. In danbauk, chicken specially seasoned with a danbauk masala spice mix, is cooked with the rice. Danbauk is typically eaten with a number of side dishes, including a fresh salad of sliced onions, julienned cabbage, sliced cucumbers, fermented limes and lemons, fried dried chilies, and soup. In recent decades, danbauk restaurants have innovated variations, including "ambrosia" biryani, which features dried fruits and buttered rice.

West Asia
In Iraq and in the states of the Persian Gulf, biryani (برياني: "biryani") is usually saffron-based with chicken usually being the meat or poultry of choice. It is popular throughout Iraq, especially in the Kurdistan Region. Most variations also include vermicelli, fried onions, fried potato cubes, almonds, and raisins spread liberally over the rice. Sometimes, a sour/spicy tomato sauce is served on the side (maraq).

In Iran, during the Safavid dynasty (1501–1736), a dish called Beriyan Polo (Nastaliq script: ) was made with lamb or chicken, marinated overnight—with yogurt, herbs, spices, dried fruits like raisins, prunes or pomegranate seeds—and later cooked in a tannour oven, then served with steamed rice.

Afghan biryani
A different dish called biryan is popular in Afghanistan. Biryan traces its origins to the same source as biryani, and is today sold in Afghanistan as well as in Bhopal, India. Biryan is prepared by cooking gosht and rice together, but without the additional gravy (yakhni) and other condiments that are used in biryani. The Delhi-based historian Sohail Hashmi refers to the biryan as midway between pulao and biryani. Afghan biryani tends to use much dry fruit such as raisins and lesser amounts of meat, often cut into tiny pieces.

Indonesia
Nasi kebuli is an Indonesian spicy steamed rice dish cooked in goat meat broth, milk and ghee. Nasi kebuli is descended from kabuli palaw which is an Afghani rice dish, similar to biryani served in the Indian subcontinent.

Although Indonesia has authentic nasi kebuli, Indonesia also inherited and has local-style of biryani which is known as nasi biryani or nasi briyani. Nasi biryani is popular among and often associated as Acehnese, Arab Indonesian, Indian Indonesian and Malay cuisine.

Malaysia and Singapore
The Malaysian and Singaporean variety of biryani is called nasi briyani or nasi biryani. Although authentic styles of biryani from South India are popular, nasi briyani remains the most popular. The key differences between nasi briyani and Indian biryanis are that the meat in nasi briyani is cooked separately from the rice, and there is more curry, sauce, or gravy present in the nasi briyani than in Indian biryanis.

Nasi briyani dishes are very popular in Malaysia and Singapore. As an important part of Malaysian and Singaporean Indian cuisines, they are popularized through mamak stalls, hawker centres, and food courts as well as fine dining restaurants.

There are also eateries that sell pork as the main meat of the dish in Singapore.

Mauritius
Biryani dishes are very popular in Mauritius, especially at Muslim weddings and festivities. It is also widely available at street food places. Mauritian biryanis are often accompanied by an achaar (mango pickles), chilies and salads.

Philippines
Kapampangan cuisine of the Philippines (often in Pampanga) features a special dish called nasing biringyi (chicken saffron rice), that is typically prepared only during special occasions such as weddings, family get-togethers or fiestas. It is not a staple of the Filipino diet as it is difficult to prepare compared to other usual dishes. Nasing biringyi is similar to the nasi briyani dish of Malaysia in style and taste. A version that has merged with the Filipino version of the Spanish paella is known as bringhe.

South Africa
In the Cape Malay culture, a variation of biryani incorporates lentils as a key ingredient in the dish along with meat (usually beef, chicken, seafood or vegetables). The dish is made by cooking the rice and legumes and meat and gravy separately, then mixing it. Uncommonly, it is made using the dum-cooking method. The spices are similar to those used in the original Indian biryani.

East Africa
Variants of biryani exist in the cuisines of Somalia, Kenya, and Tanzania due to centuries of trade between the East African coast and South Asia for centuries, and the more recent migration of Indians to the latter two countries more recently during the British colonial era.

Zanzibar has its own form of biryani characterized by the mixture of East African and Indian spices, as well as influences from Arab cuisine. The meat used is most commonly chicken. This variant is similar to the forms of biryani served in Kenya.

In Somalia, the descendant of biryani is bariis iskukaris. It is served with chicken, goat, beef, lamb, or camel meat, and spiced with the Somali spice mixture xawaash and other spices. A unique characteristic of bariis and other Somali dishes is the addition of banana on the side to be mixed with the dish.

Thailand
Biryani in Thailand is commonly known as khao mhok (ข้าวหมก). It is commonly paired with chicken, beef or even fish and topped with fried garlic. The dish is common in Thai cuisine and is often served with a green sour sauce.

Tehari
Tehari and tehri are various names for the vegetarian adaptation of Biryani but are mainly classified as pulao. It was developed for the Hindu bookkeepers of the Muslim Nawabs. It is prepared by adding potatoes to the rice, as opposed to the case of biryani, where the rice is added to the meat. In Kashmir, tehari is sold as street food. Tehari became more popular during World War II, when meat prices increased substantially and potatoes became the popular substitute in biryani.

title: Biryani


text:
Category:Underground cities

For more information, see the article Underground city.

title: Category:Underground cities