Q:

Reference: Beth Trees in Propositional Logic

I am looking for a reference on so-called ''Beth trees''.
Take a finite set of propositional formulas $\mathcal{F}$. As an example, we might be looking for the set of valuations $v$ that satisfy every formula in $\mathcal{F}$. A Beth tree is a type of parse tree that allows us (in a syntactic manner) to find such valuations. A vertical bar separates the formulas we want to be true from the formulas we want to be false. In the case outlined above, we'd write down all formulas of $\mathcal{F}$ to the left of the vertical bar, and the empty set to its right. Then we parse the formulas one by one. Some examples (in the following, $F$ is assumed to be to the left of the vertical bar; some rules would flip for $\lor$/$\land$ when $F$ is assumed to be on the right):

if $F$ is a propositional variable, we don't do anything as each valuation is uniquely defined by what it does to propositional variables
if $F$ is $\lnot G$ then $$F, F_1, \ldots, F_n \mid E_1, \ldots, E_m$$ becomes $$F_1, \ldots, F_n \mid G,E_1, \ldots, E_m$$ in a new branch below
if $F$ is $G \lor H$ then we know that either $G$ or $H$ must be true. So we have two branches so that $$F, F_1, \ldots, F_n \mid E_1, \ldots, E_m$$ becomes $$G,F_1, \ldots, F_n \mid E_1,\ldots ,E_m$$ on one branch and $$H,F_1, \ldots, F_n \mid E_1,\ldots ,E_m$$ on the other
if $F$ is $G \land H$ then we know that both $G$ and $H$ must be true, so we replace $$F, F_1, \ldots, F_n \mid E_1, \ldots, E_m$$ by $$G,H,F_1, \ldots, F_n \mid E_1,\ldots ,E_m$$ in a new branch below
if we have a propositional variable $P$ both to the left and to the right of the vertical bar, we can stop as this branch does not give rise to a valuation (we would have $v(P) = 1 = 0$)

Clearly, this is a more visual representation of the method of analytic tableaux. But I have heard the term Beth tree for this type of algorithmic procedure in tree form before -- has anyone seen the term before describing the tree algorithm outlined above?

A:

I guess you refer to the original definition of semantic tableaux given by E. W. Beth in Semantic entailment and formal derivability (1955), which had been later simplified by R. Smullyan in First-order logic (1968) to the widespread definition of semantic tableaux commonly used in logic.
A good reference that traces the introduction and evolution of this tree method for satisfiability and provability is: I.H. Anellis, From Semantic Tableaux to Smullyan Trees. A History of the Development of the
Falsifiabitity Tree Method (1990).
It contains also a comprehensive bibliography on the topic.

