Tableaux

https://en.wikipedia.org/wiki/Method_of_analytic_tableaux

In proof theory, the semantic tableau (truth tree) is a decision procedure for sentential and related logics, and a proof procedure for formulae of FOL.

An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the satisfiability of finite sets of formulas of various logics.