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.

Architecture

The TWB is organised into four main components which total roughly 4000 lines of Ocaml code (loc). The core (464 loc) contains all type definitions and the strategy implementation. The data-type library (664 loc) implements support data structures. The tableau library (818) provides the machinery to implement tableau-based provers. The syntax library (1624) provides an easy way to access the TWB library and to define specific logic modules. Finally the command line interface (226 loc) provides a simple shell interface for compiling and executing the logic modules on input formulae. The core library defines the architecture of the prover using abstract data types. The core library is composed of the following modules: *Sequence: Since OCaml is by design an eager language, we avoid wasteful computations by using a generic lazy list (library) to construct the proof tree; * Tree: Defines the proof tree data type; * Node: Defines a node as a generic container which encapsulates arbitrary data structures (like sets, multi-sets, sequences, etc.); * Rule: Implements the interface to define logical rules in the TWB. A rule can be seen as a re-writing function that is applied if a pre-condition is met. Defines the interface for specifying rules; * Visit: The Visit module implements the core algorithm to generate and visit the proof tree given the current node and the current state of the strategy.

Core Algorithm

[inline:algorithm.gif] The core algorithm of the TWB is a procedure to visit a tree that is generated by the repeated application of a finite set of rules to an initial node containing a finite number of formulae. The visit procedure is basically an interpreter for the strategy language. Given the state of the strategy and the current node returns the result of the visit of the tree generated by applying the strategy to the current node. The strategy embedes the tableau/sequent rule to be applied following the specification language in [[defining_strategy]]. In principle, the end result of the visit procedure is a list of results as the '''alt''' operator of the strategy effectively is a branching operator at the strategy level. However, since the alt operator is always guarded by an acceptance condition, only one result is selected from a strategy even when both alternations are equally applicable. In the figure above, we show a snapshot of the visit procedure by focusing on a node in the proof tree (the ''current node''). * Rule condition: this function is used by the strategy procedure and checks if a rule is applicable to the current node and if the side conditions of the rule are satisfied. The result of this function is a partition of the current node according to the patterns specified in the numerator of the selected rule. * Rule action: this function accepts a rule that has been selected and applies it to the current node to expand the proof tree. The result of this function is a list of nodes, each identifying a new branch in the proof tree. *Branch condition: this function is executed after visiting the i^th sub-tree rooted at the current node to determine if the sub-tree created so far (including all the already visited branches) satisfies a logic-specific condition. If so, the visit explores the next branch (if any), otherwise, the visit is interrupted and the procedure backtracks. * Rule backtrack: these functions are executed after all branches (or a number of them according to the branch condition) are visited to synthesise their results into one result for the current node and pass it up to its parent.

Removing Non-Determinism

A ''don't care'' non-deterministic choice is an arbitrary choice of one among multiple possible continuations for a computation, all of which return the same result. A ''don't know'' non-deterministic choice is one choice among multiple possible continuations, which do not necessarily return the same result. For completeness in a tableau calculus, it is sufficient to assume that all choices are ''don't know'' non-deterministic. However, a deterministic algorithm based on this assumption will be extremely inefficient since it has to consider all possible continuations for all choices. Thus it is imperative to remove as many forms of non-determinism as possible. Traditionally, logicians focus on the existence of a derivation tree rather than on how it is found. Conversely, automated reasoners focus on designing algorithms to search for a derivation tree as efficiently as possible. From a theoretical perspective, it is therefore not important to specify the order in which rules are applied or how the proof tree is explored. Practically, however, specifying a particular rule order can dramatically speed up the search and construction of a proof tree. Moreover, since different rule orders can produce different derivation trees, an efficient decision procedure should always try to build the smallest derivation tree. In general, we can identify three forms of non-determinism associated with three fundamental aspects of a generic decision procedure: *Node-choice: the algorithm chooses which leaf becomes the current node; *Rule-choice: the algorithm chooses which rule to apply to the current node; *Instance-choice: the algorithm chooses which formula to make the principal formula for the chosen rule and the chosen current node. That is, it determines the order in which to explore the different instantiations (partitions) of the current node created by the chosen rule. ==Node-choice== The first source of non-determinism is which (leaf) node to select as the current node and is usually handled by a visit algorithm that selects this node out of possibly many in the current tree. For exposition, we use a depth first visit function that deterministically selects the left most node, but our algorithm allows any visit strategy to be used to explore the search space (ie. breadth-first). ==Rule-choice== The second source of non-determinism in tableau methods arises from the lack of guidance when applying logical rules. If a node contains many different formulae, then many rules may be applicable to that node. How to choose? For example, in classical propositional logic, where all rules are invertible, the order in which rules are applied is not important. However specifying a strategy that applies all linear rules and the axiom first, and then all branching rules, can potentially shorten the proof tree. The problem is however different in basic modal logic, where not all sequences of rule applications ensure a solution since the (K)-rule is not invertible. The problem is even more complicated in tableau-sequent calculi with more than one non-invertible rule: for example intuitionistic logic. In this situation, at any given choice point, after all invertible rules are applied, we are forced to guess which non-invertible rule to apply, and eventually to undo this decision if it does not lead to the construction of an acceptable proof tree. Consequently, if the proof tree obtained from the application of the first rule of a sequence of non-invertible rules does not respect a logic-specific condition, the entire proof tree generated from that rule application must be discarded. To recover from this wrong choice, the proof must be re-started using the next non-invertible rule available in the sequence. Thus, for efficiency, tableau rules must be coupled with a ''strategy'' to control the order in which rules are applied. ==Instance-choice== The third form of non-determinism is the aforementioned choice of one rule instance (partition) of the current node from potentially many rule instances (partitions) of the current node. Then, this nondeterminism can be resolved by using optimisation techniques based on logic-specific considerations used to reduce the size of the search space. For example, if the chosen rule is an Or-rule, heuristics such as MOMS (Maximum number of Occurrences in disjunctions of Minimum Size) or iMOMS (inverted MOMS) order the disjunctions (formulae) in the node to always choose the less/more constrained disjunct, which, in principle, should lead to an earlier clash.

Backtracking

The underlying engine contains a backtracking procedure which is turned on as soon as a closed node is found and as soon as no rule is applicable to a node. Each of the three forms of non-determinism give rise to And-branching. That is: - choosing different current nodes will give rise to different tableaux; - choosing different rules to apply to the current node will give rise to different tableaux; - choosing different principal formulae for the chosen rule and the chosen node will give rise to different tableaux. But we need only one of these tableaux to close. Thus we have the following backtracking principle: backtrack over all choice points until we find a tableau such that each And-node has at least one closed child and each Or-node has all children closed. At any stage, if the backtracking algorithm finds a closed tableau, then it stop backtracking and simply returns closed. Conversely, as long as it fails to find a closed tableau, it continues to backtrack over all choice points. Thus, on the way down, strategies tell us how to construct the current tableau and how to leave And- and Or- choice points in creating the tableau. During backtracking, some of these choice-points are activated, as long as we have not found a closed tableau.