Core Algorithm

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 three main decisions to make are: which leaf to choose as the current node; which rule to apply to the chosen node; and which principal formula to choose from the chosen node for the chosen rule. This visit procedure is composed of two ''recursive functions'': the first function selects a new rule to be applied to the current node while the second function traverses the tree generated by the application of the rule, by recursively calling the visit procedure. In the figure above, we show a snapshot of the visit procedure by focusing on a node in the proof tree (the ''current node''). The visit procedure uses the following four basic components: * 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.