命題論理の論理式が証明可能かを判定する関数
最小の構成ならこれで良いはず
論理式$ f \in \Deltaに関してこの論理式が証明可能かどうかをチェックする関数$ v: \Delta \mapsto \{\top,\bot\}を考える
$ \vdash fなら$ \top，$ \not\vdash fなら$ \botを返す
面倒なので論理式で用いる記号を$ \{ \land, \lor, \lnot \}に縛る
先に$ \to, \leftrightarrowは次で変換しておく
適当な論理式$ \phi, \psiとして
$ \phi \to \psi = \lnot \phi \lor \psi
$ \phi \leftrightarrow \psi = (\phi \land \psi) \lor (\lnot\phi \land \lnot\psi)
構成可能な論理式集合$ \Deltaに関して
命題$ p,q,\cdotsか命題否定$ \lnot p,\lnot q\cdotsだけの集合を$ \Delta_P
$ \Delta_P = \{ p, q, \lnot p, \cdots \}
それ以外の$ \Delta - \Delta_Pを$ \Delta_{\bar{P}}
$ \Delta_{\bar{P}} = \{ p \land q, p \lor q, \lnot\lnot p, \lnot (p \land q), \lnot (p \lor q), \cdots \}
適当な論理式$ \phi, \psiで$ \phi \lor \psiと表せるような論理式だけの集合を$ \Delta_{\lor}とする
$ \Delta_{\lor} = \{ p \lor q, \cdots \}
$ \Delta_{\bar{P}, \bar{\lor}} := \Delta_{\bar{P}} - \Delta_{\lor}とする
$ \Delta_{\bar{P}, \bar{\lor}} = \{ p \land q, \lnot\lnot p, \lnot (p \land q), \lnot (p \lor q), \cdots \}
当然ながら$ \Delta = \Delta_P \cup \Delta_{\lor} \cup \Delta_{\bar{P},\bar{\lor}}
今，この$ \Deltaは入力の$ fに現れる命題記号$ p,q,\cdotsから構成される論理式という意味で，本来$ \Delta_fとでも書くべきだが，まあ明らかなので以下でも$ \Deltaと略記する
ブランチ$ Bは次の4要素の組である$ B = \lang \Gamma_t, \Gamma_s, P, J\rang
$ \Gamma_t, \Gamma_sは論理式の集合
評価待ちの論理式の集合$ \Gamma_t \sub \Delta
次の分岐のためのバッファ$ \Gamma_s \sub \Delta_{\lor}
$ P \sub \Delta_P
$ J
適当なブランチ$ B_L,B_Rとして$ \{ B_L, B_R \}，
または$ \empty
例えば
$ B=\lang \{\lnot (p \land q)\}, \{p \lor q\}, \{q, \lnot q\}, \emptyset\rang
$ B=\left\lang \left\{\right\}, \left\{\right\}, \left\{p, q\right\}, \left\{ \left\lang \left\{\right\}, \left\{\right\}, \left\{p, q, \lnot p\right\}, \emptyset \right\rang, \left\lang \left\{\right\}, \left\{\right\}, \left\{p, q, \lnot q\right\}, \emptyset \right\rang \right\} \right\rang
$ \Delta_{\bar{P},\bar{\lor}}内の論理式に関する評価関数$ e_{\Delta_{\bar{P},\bar{\lor}}}: \Delta_{\bar{P},\bar{\lor}} \mapsto \Delta^n
ただし$ nは以下より明らかに1か2
適当な論理式$ \phi, \psi
入力される論理式$ fは4パターンしかなく，それぞれについて以下を返却
$ f = \phi \land \psiなら$ \{ \phi, \psi \}
$ f = \lnot (\phi \land \psi)なら$ \{ \phi \lor \psi \}
$ f = \lnot(\psi \lor \psi)なら$ \{ \phi, \psi \}
$ f = \lnot \lnot \phiなら$ \{\phi\}
再帰的ブランチ評価関数$ e_B: B \mapsto Bを考える
入力のブランチを$ B_i=\lang {\Gamma_t}_i, {\Gamma_s}_i, P_i, J_i\rangとする
$ {\Gamma_t}_i \neq \emptysetなら$ f \in {\Gamma_t}_iとして
$ f \in \Delta_{P}
$ e_B\left( \left\lang {\Gamma_t}_i - f, {\Gamma_s}_i, P_i + f, J_i \right\rang\right)を返す
$ f \in \Delta_{\lor}
$ e_B\left( \left\lang {\Gamma_t}_i - f, {\Gamma_s}_i + f, P_i, J_i \right\rang\right)を返す
$ f \in \Delta_{\bar{P},\bar{\lor}}
$ e_B\left(\left\lang {\Gamma_t}_i - f \cup e_{\Delta_{\bar{P},\bar{\lor}}}(f), {\Gamma_s}_i, P_i, J_i \right\rang \right)を返す
$ {\Gamma_t}_i = \emptyset, {\Gamma_s}_i \neq \emptysetなら$ f' \in {\Gamma_s}_iとして
$ \left\lang \emptyset, \emptyset, P_i, \left\{e_B\left(\left\lang {\Gamma_t}_i, {\Gamma_s}_i - f', P_i, \emptyset \right\rang \right), e_B\left(\left\lang {\Gamma_t}_i, {\Gamma_s}_i - f', P_i, \emptyset \right\rang \right) \right\} \right\rangを返す
このときこの関数の定義および与える初期値から$ J_i = \emptysetであることが保証されている
親ブランチ先頭の前2組$ {\Gamma_t}_i, {\Gamma_s}_iは以降特に使わないので$ \emptyset以外の何でも構わない
それ以外，つまり$ {\Gamma_t}_i = \emptyset, {\Gamma_s}_i = \emptysetなら$ B_{i}を返す
この関数は一応どこかのタイミングで停止するはずである
再帰的ブランチ証明可能判定関数$ v_B: B \mapsto \{\top,\bot\}
入力$ B_iの$ P, Jそれぞれを$ {B_i}.P, {B_i}.Jと表すとして
$ {B_i}.J = \emptysetなら
$ \exists x. (x \in {B_i}.P \land \lnot x \in {B_i}.P)が真なら$ \botを出力
そうでないなら$ \topを出力
$ {B_i}.J = \{B_L,B_R\}なら
次のどちらかが真なら$ \botを出力
$ \exists x. (x \in {B_i}.P \land \lnot x \in {B_i}.P)が真
$ v_B(B_L) = \bot \lor v_B(B_R) = \botが真
そうでないなら$ \topを出力
この関数も，一応どこかのタイミングで停止するはずである
問題の論理式$ f \in \Deltaについて
$ e_B(\lang \{\lnot f\}, \emptyset, \emptyset, \emptyset\rang)で完成形のブランチ$ B_{\lnot f}を得る
$ v_B(B_{\lnot f}) = \botなら元の$ fは証明可能である
ただし，このままだと元の$ fについて$ \botという結果が返ってきて見た目が良くない
反転関数$ i:\{\top,\bot\}\mapsto \{ \top,\bot\}を噛ます
$ \topなら$ \botを返却
$ \botなら$ \topを返却
つまり$ v: \Delta \mapsto \{\top,\bot\} = i(v_B(e_B(\lang \{\lnot f\}, \emptyset, \emptyset, \emptyset\rang)))としたとき
$ vは論理式$ f \in \Deltaが証明可能か判定する関数である
$ e_B, v_Bが停止するので，この関数は停止するはず
備考
実運用上，あるいはタブローの形式的表現としては
ブランチの定義を拡張して前状態の論理式を保存するための，プログラミング言語のリストに近い$ \Gamma_Lみたいなものを考える必要があるが，面倒なので一旦それは飛ばした