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

# on 31 May 2004, 00:28

Couldn't find a trackback url, so:

# on 31 May 2004, 16:57

are the valid formulas for which there aren't terminating tableaux second-order or first-order? the fact that second-order logic is undecidable is the reason there exists non-terminating tableaux for valid formulas in second-order logic. it isn't a problem concerning the method of systematically expanding (into subformulas) and closing a tableau; rather, it's a problem with 2nd-order logic itself.

i am greatly certain u're aware of this, in which case, i must've misinterpreted the beginning of your post.

(i wish also to discuss penis enlargement, possibly over a cup of frothy latte.)

# on 01 June 2004, 05:21

then again, first-order arithmetic is undecidable as well.

# on 01 June 2004, 11:08

Doesn't Blogger find the trackback URL in the sourcecode by itself? I always thought displaying trackback URLs to human users was just a marketing ploy by MT to push their trackback standard.

muxol, the prover is a prover for classical first-order validity (which is of course also undecidable).

Anyway, I've since given up the strategy described here and implemented the common algorithm of trying out all possible tableaux. (On the hard disk in the dead computer -- I hope it has survived!)

# on 07 June 2004, 16:51

actually, first-order propositional logic is decidable, whereas first-order predicate logic isn't.