Basic Notions

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.