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 Patel-Schneider 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 [](-[](p|q)|-[](p|r)), 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 tableaux-based 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 |