Suppose the current branch of the tableaux contains the disjunctions (p  q) and (p  r). The standard disjunction elimination rule, also called syntactic branching rule, will create one branch on which p is true and one branch on which q is true. Suppose the first branch can be closed and that we need to consider the second branch. The syntactic branching rule creates one branch on which p is true and one branch on which r is true. It is straightforward to see that we are able to close the first branch again, possible constructing a large tableaux to do so, before we turn to the second branch.
The solution proposed by Giunchiglia and Sebastiani (1996b) is to use a semantic branching rule. Here, in the presence of (p  q) and (p  r) we create two branches, one on which p is true and one on which p is true. The formula p is called cut formula. Again, we assume that the first branch can be closed. On the second branch, however, no further application of the branching rule is necessary. Instead we use the simplification rules described before, to replace (p  q) and (p  r) by q and r. No additional branches are created and it seems that unnecessary search is avoided.
Similar observations also appear in various papers by Horrocks and PatelSchneider to justify the use of semantic branching in the systems FaCT and DLP. However, the authors also observe that the use of semantic branching is most effective with randomly generated problems and less with realistic description logic knowledge bases.
While the considerations above are correct for tableaux calculi for propositional logic in clausal form, it seems to be quite commonly known that the situation for other logics is not that simple. In the case of modal logics, the cut formula can be a complex modal expression which itself or its negation, introduces additional branches into a tableaux. For example, if the cut formula is []([](pq)[](pr)), then creating one branch on which this true and a second one on which it is false, might actually create a tableaux with a higher number of branches than the one we obtain using syntactic branching.
To investigate the effect of these two variants of disjunction elimination we compare two tableauxbased systems which are identical except that one system uses semantic branching while the other one uses syntactic branching. We first consider the 90 percent percentile for these systems on PS0 (N=5, M=1, K=3, D=2, P=0.5) and PS14 (N=10, M=1, K=3, D=2, P=0.5).
Next we look at the 50 percent and 90 percentile graphs for these systems on random formulae generated with our modified random generator for the parameter settings (N=4, M=1, K=3, D=1, P=0) and (N=6, M=1, K=3, D=1, P=0).
Examples on which syntactic branching performs better than semantic branching can be found in the benchmark collection of the Logics Workbench.
Class  Number 



k_d4_p  1  0.000  0.000  
k_d4_p  2  0.070  0.060  
k_d4_p  3  1.310  1.060  
k_d4_p  4  26.860  16.930  
k_d4_p  5  465.410  266.740  
k_d4_p  6  8171.290  4130.150  
k_d4_p  7  137874.600  60307.840 
Class  Number 



k_t4p_p  1  0.070  0.040  
k_t4p_p  2  0.230  0.160  
k_t4p_p  3  0.550  0.420  
k_t4p_p  4  2.150  1.530  
k_t4p_p  5  8.680  5.860  
k_t4p_p  6  34.670  23.180  
k_t4p_p  7  138.690  92.460  
k_t4p_p  8  554.810  369.380  
k_t4p_p  9  2222.900  1481.550  
k_t4p_p  10  8911.430  5939.040  
k_t4p_p  11  35662.810  23740.240  
k_t4p_p  12  148870.000  96397.520 