Definition
Closed Branch (First-Order Tableaux)
A branch in a first-order tableau is closed when it contains both
and for some formula . A tableau is closed when all of its branches are closed. A closed tableau certifies that the initial formula is unsatisfiable.