# Semantic versus syntactic branching

Giunchiglia and Sebastiani (1996b) pointed out a particular weakness of previous implementations of tableaux-based theorem provers like KRIS or the Logics Workbench.

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).

As we can see there is no noticable difference between the two systems.

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).

Here we see a clear advantage of semantic branching over syntactic branching.

Examples on which syntactic branching performs better than semantic branching can be found in the benchmark collection of the Logics Workbench.

Figure 10: Syntactic vs. Semantic branching on k_d4_p and k_t4p_p
ClassNumber
 Runtime (in seconds) Semantic branching
 Runtime (in seconds) Syntactic branching
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
ClassNumber
 Runtime (in seconds) Semantic branching
 Runtime (in seconds) Syntactic branching
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

There are in fact a number of results on various optimisations of the syntactic branching rule in clausal tableaux calculi for propositional logic. See, for example, the chapter of Letz and Stenz in the upcoming Handbook of Automated Reasoning. Letz and Stenz consider factorisation, folding down (which corresponds to semantic branching), and folding up.
Top: Contents | Previous: Revised comparison of modal theorem provers | Next: References
[an error occurred while processing this directive]