Closed Branch (First-Order Tableaux)

first-order-logic tableaux

Definition

Closed Branch (First-Order Tableaux)

A branch in a first-order tableau is closed when it contains both $t:\phi$ and $f:\phi$ for some formula $\phi$.

A tableau is closed when all of its branches are closed. A closed tableau certifies that the initial formula is unsatisfiable.