Tableaux

Origin. Beth (1955), Smullyan (1968). Tree-based proof search. Formulas labeled signed. Branch closure for contradiction. Foundation for automated reasoning.

Models. Systematic decomposition. Signed formulas: T:φ or F:φ. α-rules (non-branching), β-rules (branching). Closed tableau = proof.

Formalism.

Signed formulas: T:φ (φ is true) F:φ (φ is false)

α-rules (conjunctive): T:A ∧ B → T:A, T:B (same branch) F:A ∨ B → F:A, F:B F:A → B → T:A, F:B T:¬A → F:A

β-rules (disjunctive): F:A ∧ B → F:A | F:B (split branches) T:A ∨ B → T:A | T:B T:A → B → F:A | T:B F:¬A → T:A

Branch closure: Branch closed if contains T:A and F:A. Tableau closed if all branches closed.

Completeness: Closed tableau for ¬φ proves φ. Open branch → countermodel.

First-order: γ-rules: T:∀xA, F:∃xA (instantiate any term) δ-rules: F:∀xA, T:∃xA (fresh variable)

Modal tableaux: Labeled formulas: w:φ Accessibility: wRv Rules propagate across worlds.

Symbols.

Symbol	Unicode	Name	Meaning
T:	—	True	Signed true
F:	—	False	Signed false
α	U+03B1	Alpha	Conjunctive rule
β	U+03B2	Beta	Disjunctive rule
×	U+00D7	Closed	Contradiction

Metatheory. Sound and complete for classical/intuitionistic/modal. Termination with loop checks. Decidability for propositional. Proof extraction.

Applies to. Automated theorem proving. Logic education. Model generation. Decision procedures. Interactive provers.

Limitations. Inefficient naive implementation. Loop detection needed. First-order non-terminating. Optimization required.