Open Branch (First-Order Tableaux)

first-order-logic tableaux

Definition

Open Branch (First-Order Tableaux)

A branch in a first-order tableau is open when it is complete (no further rules can be applied) and contains no pair $t:\phi$ and $f:\phi$ for the same formula $\phi$.

An open branch certifies that the initial formula is satisfiable.