§10.3.5 of Logic: The Laws of Truth by Nicholas Smith specifies a procedure for extending an unfinished tree in such a way that the resulting tree is guaranteed to be finished.
An abridged version of the procedure is as follows:
PHASE 1: Give each proposition in the tree an address:
The first root proposition has address 1.
Any proposition $%alpha$ in the tree (apart from the first) is given an address as follows:
i) If the proposition lies immediately below another proposition with addr $n$, then its addr is $n1$.
ii) If the proposition lies on the immediate left of another proposition with addr $n$, then its addr $n1$.
iii) If the proposition lies on the immediate right of another proposition with addr $n$, then its addr is $n2$.
PHASE 2: Extend the tree according to the following procedure:
Go through every proposition in the tree on order of address. For each proposition $%alpha$ that you visit:
i) If $%alpha$ lies on no open path, or $%alpa$ is an atomic proposition or a negated atomic proposition, or $%alpha$ had been checked off, then move on to the next proposition. Otherwise stay on $%alpha$ and go to step (ii).
ii) If $%alpha$ can have a connective rule or a negated quantifier rule applied to it, apply this rule at the bottom of every open path on which $%alpha$ lies, and check $%alpha$ off.
If $%alpha$ can have the unnegated quantifier rule applied to it, apply this rule to the bottom of every open path on which $%alpha$ lies, using the alphabetically first name that doesn't appear on the path, and check $%alpha$ off.
If $%alpha$ can have the unnegated universal quantifier rule applied to it, apply this rule to te bottom of every open path on which $%aplha$ lies, one for each name that appears on the path, but only if the resulting formula does not already appear on the path. If no names appear on the path, apply the rule using the name $a$. Since $%alpha$ is a universally quantified wff, do not cross it out.
Each time we add a wff to an open path, check the path for closure.
Once all the propositions in the tree have been processed, go to step (2).
If the tree has changed in any way (e.g. you added new propositions, closed a path, checked off a wff, etc.), go back to step (1). Otherwise, stop.
From what I understand, the reason that this procedure guarantees that the resulting tree is finished is that it forces us to visit every wff in the tree on each iteration of step (1), so that no wff is left unprocessed.
The next section (§10.3.6) discusses the problem of finding a pattern in the tree:
In the previous section, we solved one of our two problems: coming up with a strategy for extending a finite initial section of a tree in a way that ensures a finished tree. Now to the next problem: how do we detect what pattern emerges from this strategy, so that we can read off a model? Here the new is not so good. We have an effective procedure for extending any finite segment of a tree to a finished tree. But there is no effective procedure that tells whether - when finished - the tree will have an infinite path. It is not just that no one has come up with such a procedure, it has been shown that there cannot be such a procedure.
In a later chapter, this result is introduced as the undecidability of first order logic. However, I'm unclear regarding the gist of the above excerpt. How would a procedure that tells us whether or not a tree is infinite help us discern the pattern in that tree? Is it simply because such a procedure would have to be able to identify cycles in the output?
Also, isn't the algorithm given in §10.3.5 (as outlined in the post) one such procedure? It guarantees that the resulting tree is finished, so if we apply it to a tree and find that we keep looping back to step (1), then we can be sure that the tree is finished and infinite?