Soundness and Completeness of Semantic Tableaus
Jump to navigation
Jump to search
Theorem
Let $\mathbf A$ be a WFF of propositional logic.
Let $T$ be a completed semantic tableau for $\mathbf A$.
Then $\mathbf A$ is unsatisfiable if and only if $T$ is closed.
Corollary 1
$\mathbf A$ is satisfiable if and only if $T$ is open.
Corollary 2
$\mathbf A$ is a tautology if and only if $\neg \mathbf A$ has a closed tableau.
Proof
The two directions of this theorem are respectively addressed on:
$\blacksquare$
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.7$: Theorem $2.67$