Definition
Splitting Tree (Propositional Logic)
The splitting tree of a propositional formula
is the binary tree built by repeated splitting:
- the root is
; - a constant node is a leaf —
marks a satisfiable branch, an unsatisfiable one; - any other node
branches on an atom occurring in into the two children and . Each branch step removes one atom, so the depth of the tree is at most the number of atoms of
. Every root-to-leaf path fixes the truth values of the atoms it branches on, so a leaf witnesses a satisfying assignment.