Splitting Tree (Propositional Logic)

Definition

Splitting Tree (Propositional Logic)

The splitting tree of a propositional formula $A$ is the binary tree built by repeated splitting:

• the root is $A$;
• a constant node is a leaf — $\top$ marks a satisfiable branch, $\perp$ an unsatisfiable one;
• any other node $B$ branches on an atom $p$ occurring in $B$ into the two children $B_p^{\top }$ and $B_p^{\perp }$.

Each branch step removes one atom, so the depth of the tree is at most the number of atoms of $A$. Every root-to-leaf path fixes the truth values of the atoms it branches on, so a $\top$ leaf witnesses a satisfying assignment.