A graphical representation of a partially built propositional tableau In proof theory, the semantic tableau[1] (/tæˈbloʊ, ˈtæbloʊ/; plural: tableaux), also called an analytic tableau,[2] truth tree,[1] or simply tree,[2] is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic.[1] An analytic tableau is a tree structure computed for a logic