Warnings for overlapping or inexhaustive rules

[nsbgn]

When designing a tableau system, there are two peculiarities that can arise.

First, the rules might not be exhaustive, that is, there might not be a rule for all polarities and primitive connectives. This might be intended, as indeed it is for J; the most we can do is issue a warning.

We might also have overlapping rules, that is, two rules may be applicable to (some) of the same formulas on the branch. Note that this is different from having a rule with multiple instances, since rules may overlap without being an instance of the same meta-rule. It will be helpful to issue a warning in these cases.

Moreover, we might want to change a setting to determine whether these cases are to be handled nondeterministically or greedily, in much the same way that rule instances might be handled nondeterministically or greedily.

[nsbgn]

Overlapping rules should issue more than just a warning: they should be allowed in the first place. A separate +R and +L rule is impossible at this point, because nondeterminism is only allowed in rules of the same instance.