Wolfgang Schwartz asks here if there is a “canonical” way to build free-variable tableaux which are guaranteed to close if the original formula is valid. It seems to me that this must be the case, since free-variable tableaux are a complete proof method. But maybe I don’t understand the question.
The point of free-variable tableaux is to postpone substitutions of strong quantifiers until such a substitution results in a closed branch. So instead of expanding a branch containing ∀x A(x) by A(t) for all possible t, you keep the free x around until you get a formula ¬ B on the branch where A(x) and B unify. Closure, i.e., the actual substitution of x by a term only happens when this is the case. So at each stage, you should check if you can apply Closure (i.e., if you can close the branch) but you don’t actually apply it until you can.