Definition
Closed Branch
A branch in a semantic tableau is closed when it contains both and for some formula . This represents a contradiction: the same formula cannot be both true and false under one interpretation.
A tableau is closed when all of its branches are closed.
Relation to Satisfiability
Unsatisfiability Witness
A closed tableau certifies that the initial formula is unsatisfiable. Each closed branch identifies a specific contradiction that prevents any model from satisfying the formula.
If any branch remains open after all rules are applied, the formula is satisfiable. The open branch provides a model: assign to every atom where appears, and to every atom where appears.