Core Algorithm

NOT FOUND: 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.