Method of analytic tableaux

Analytic tableau, or more briefly, just tableaux, are a fundamental approach in automated theorem proving that provide a rich source of decision and semi-decision procedures for various logical calculi, such as propositional logic, intuitionistic logic, first-order logic and modal logic. The fundamental idea behind analytic tableau derives from the cut-elimination theorem of structural proof theory.