A truncation technique for clausal analytic tableaux (Q1198076)

Resolution theorem proving research has developed many strategies and rules to improve the performance of the method. Many of the rules have been deletion rules which prune the search space in some way. One such rule is the merging rule which we consider. Merging is used to reduce two like literals in a clause into one. This technique is modified for analytic tableaux, however, even though the hint for developing the rule came from resolution. The modified technique is called the branch-merge rule. The analytic tableau method has a complete control structure and we show that the inclusion of the branch-merge rule does not affect this.