Restrict the Gamma Rule?
The following restriction might be a way out of the problems I mentioned in my last posting:
The gamma rule must not be applied if the result of its previous application has not yet been replaced by the Closure rule.
(The gamma rule deals with 
and 
formulae; the Closure rule is the rule that allows to replace dummy
constants by real constants iff that leads to the closure of at least one
branch.)
That restriction solves many cases where the unrestricted gamma rule leads
to infinite tableaux. It even helps with the xyFxy case
that can't be solved by the ordinary Herbrand restriction on sentence
tableaux. (On the other hand, it can't detect the satisfiability of
x((Fx
y Fy) 
Gx), which the
Herbrand restriction can. And it doesn't provide a means to read off
counter-models from open branches.)
I wonder if the restriction preserves completeness. So far I could find neither a proof that it does nor a counter-example that shows that it doesn't. Can anyone help?
[Update 2003-05-14: Reinhold Letz says he thinks the restriction is okay, but he recommends using disconnection tableaux (PDF) to detect satisfiability. However, I'd rather not translate the input formula into clausal form, because then I can't use the internally created tree as a template for the displayed tree proof (which doesn't require clausal forms).]