```
N
-----------
d1 ... dn
```

where N
is the numerator, while ''d1 ... dn'' is a list of n denominators.
The numerator contains one or more distinguished formula schemas
called ''principal formulae'' and one or more formulae schema called
''side formulae''. We use meta-variables '''A, B, P, Q, ... ''' to
represent principal formulae and '''X,Y,Z''' for, possibly empty,
"containers" of side formulae: traditionally sets, multisets or
sequences, but possibly more complex data structures for generality.
Operationally, tableau rules can be seen as functions to transform a
(container) node into a list of (container) nodes during the
construction of a graph. We say that a rule is ''applicable'' if we
can ''partition'' the contents of the current node to instantiate
the meta-variables in the numerator .
The ''denominators'' of a rule represent actions to expand the graph by
creating new nodes according to these instantiations.
The repeated application of rules gives rise to a tree of nodes, with
children obtained from their parent by instantiating a rule. To
capture sequent calculi as well as tableau calculi, we view this
process as a search for a proof where all leaves are "closed". But
in general, for tableau calculi with cyclic proofs, there are really
three notions: ''success'', ''failure'' and ''undetermined'': we
stay with the dichotomy "closed" as success (of proof search) and
"open" as failure (of proof search) for now to simplify the
exposition.
A numerator pattern like '''Z''' is ''unrestricted'' since its shape
does not restrict its contents in any way. Conversely, the pattern
'''Box X''' is restricted to contain only Box-formulae, '''X &Y''' is
restricted to contain only &-formulae while '''{A & B}''' is
restricted to contain exactly one single &-formula. Patterns
like '''X & Y''' are allowed to be empty, but '''{A & B}''' is not.
Currently, we forbid purely structural numerators like '''X;Y''' which
non-determ-inistically partition the node '''N''' into two arbitrary
disjoint containers '''X''' and '''Y''' (even though such numerators may be
useful for linear logic), and numerators like '''Box X ; Box Y; Z'''
since both can lead to an exponential number of possible different
partitions.
Consequently, the ''only'' form of non-determinism in rules
is the ''formula choice'' non-determinism in
choosing the principal formula.
More generally called ''instance choice'', this non-determinism
leads to ''implicit branching'' since the choice-point is hidden in
the pattern-matching (rule instance). We return to this issue later
after identifying the various forms of non-determinism inherent in
tableau proof search.