Definition
Branch
A branch in a semantic tableau is a path from the root to a leaf, representing a sequence of signed formulas accumulated during the tableau construction. Each signed formula on the branch is a consequence of applying tableau rules to its predecessors.
A branch is complete when no further rules can be applied to any formula on it. A branch is open if it is complete and contains no closed branch (i.e. no formula appears with both signs and ).
Properties
Open Branch as Model
An open, complete branch provides a model for the initial formula. Assign to every atom where appears on the branch, and to every atom where appears.
If all branches close, the initial formula is unsatisfiable.
Relation to Splitting
Connection to Splitting Trees
Each branch in a tableau corresponds to a leaf in the equivalent splitting tree. The tableau method and splitting algorithm perform the same case analysis, but tableaux track signed formulas directly rather than substituting truth values.