古典命題論理のタブロー飽和拡大アルゴリズム
論理式$ \varphiとチェックを表す$ \{✅,❌\}のペア$ \lang \varphi,✅ \rangまたは$ \lang \varphi,❌ \rangとする.
論理式とチェックのペアの集合$ \Gamma,\Deltaとし,タブロー$ (\Gamma,\Delta)を定める. 煩雑なのでタブローの中では$ \lang \varphi,✅ \rangを$ \underline{\varphi},$ \lang \varphi,❌ \rangを$ \varphiと書くこととする.
例えば,$ (\{ \underline{p \to q} \},\{p, \underline{q}\})などがそのようなタブローとなる.
タブローの$ \Gamma,\Deltaを走査していく.
もし$ \lang \varphi,❌ \rangなペアを発見したとき,
$ \varphiが命題変項$ pであったときは❌を✅に置き換える.
他の場合,$ \varphiの形と飽和拡大ルールにしたがってタブローを高々2個のタブローへと拡大/分岐させて走査を打ち切る. 拡大/分岐したタブローに対して同様に走査していく.
これをやっていけば,論理式が有限長および$ \Gamma,\Deltaが有限であればいずれ全て❌になったタブローが何個か生成される.
このタブローの数は高々$ 2^{\sum_{\gamma \in \Gamma}|\mathrm{Sub}(\gamma)| \times \sum_{\delta \in \Delta}|\mathrm{Sub}(\delta)|}個で収まる
各々の$ \Gamma,\Deltaの個数$ |\Gamma|,|\Delta|は有限
$ \mathrm{Var}(\Gamma) \cap \mathrm{Var}(\Delta) \neq \emptyであるタブローがあったとき,それは意味的帰結$ \Gamma \vDash \Deltaの反例モデルとなる
逆にない場合,$ \Gamma \vDash \Deltaは反例モデルを持たないすなわちこの意味論帰結は正しいこととなる