Wolfgang Schwarz

Tableaux Trouble

I have a problem with the new, free-variables powered version of my tree prover (only existing here on my hard disk at the moment): It doesn't terminate on some valid formulas, at least not within reasonable time.

A very nice feature of ordinary tableaux is that there is a mechanical procedure for building a ("canonical") tableau that will always close as long as there is any closed tableau for the input formula. To my knowledge, no such procedure has been found for free-variable tableaux. The problem, I think, is to decide at each stage whether to apply an ordinary expansion rule or the Closure rule. For many trees, it is best to apply Closure after every expansion. But for some formulas, this procedure will leave the tree forever open. The common response to this problem is apparently to try out all possible decisions at every point, using backtracking and iterated deepening of the search space.

This response doesn't use another nice feature of both ordinary and free-variable tableaux: that there are no dead-ends in the tableau construction. That is, if a tableau can be closed at all, it can be closed no matter what rules were so far used in which order. For instance, if you build a tree with the greedy Closure strategy just mentioned on a formula for which it doesn't work, but then switch to another strategy later, say after a million steps, you can still close the tree. So, I thought, why not just try out all possible strategies after each other, instead of always starting out again with the other strategies? In fact, wouldn't eventually all strategies get used at some time if the decision at every stage is randomized? That's what my prover currently does. At every stage it decides at random whether to apply Closure or expand the next formula.

However, perhaps that's a silly idea. For assume that on average, making the worse decision at a stage means that (again on average) 2 more steps are needed to close the tableau (2 more than if the other decision had been made). Since my method makes the wrong decision 50% of the time, it would then be rather likely that the tableau will grow forever.

So that's one possible reason why for some formulas, my prover doesn't terminate. (It's only a possible reason because I have no idea whether the number 2 in that reasoning is realistic.)

Another possible reason is that what I labeled with the bold-face "I think" above is wrong: I'm not sure whether it is fair to always apply Closure in a determinate way to all formulas on the tree, as I currently do. Perhaps the order of selecting formulas for Closure makes a difference, or perhaps for some proofs it is necessary that at some stage Closure is applied only once, even though it could be applied twice.

Hm.