We now discuss several aspects of tableau calculi which are important
when trying to mechanize the tableau method. We assume the reader is
familiar with tableau methods.
Tableau rules are of the form
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.