論理プログラミング(11) - エレファント・コンピューティング調査報告

逆に

$\vdash \displaystyle \exists t_1 \exists t_2 \cdots \exists t_\nu (a_1 \land a_2, \land \cdots \land a_k \rightarrow r)$

という形の列(各 $a_i$ は

$\displaystyle \forall v_{i1} \forall v_{i2} \cdots \forall v_{ih_i} \exists c_{i1} \exists c_{i2} \cdots \exists c_{ig_i} (p_{i1} \land p_{i2} \land \cdots \land p_{il_i} \rightarrow q_i)$

という形の論理式)を証明する証明図(*)が存在するとします。

$\displaystyle a_1 \land a_2, \land \cdots \land a_k$

という論理式を $\delta$ とおきます。 $\delta$ を $n$ 個並べた列を $\delta^n$ と書くことにします。

「シークエント計算」についてはほとんど説明していないし、詳しく知っているわけでもないので以下の説明はちゃんとした説明にはなっていないのですが、こういう流れだということだけ説明していきます。

証明図が存在するとき、論理式の外側に1個ずつ論理記号を追加していく形の証明図が存在します。以前の記事で PLP のプログラムから証明図を書く流れを説明しましたが、これは外側の論理記号を1個ずつ外していくものとなっていました。これを逆にたどっていくと

$\displaystyle \delta^n \vdash r$

を証明する証明図(**)が存在するならば、PLP のプログラムは成功するということがわかります。証明図(*)は

$\displaystyle \cfrac \vdots {\cfrac {\delta^n \vdash r} {\cfrac {\delta \vdash r} {\cfrac {\vdash \delta \rightarrow r} {\vdash \exists t_1 \exists t_2 \cdots \exists t_\nu (\delta \rightarrow r)} (\exists 右の繰り返し)}(\rightarrow 右)}(縮約左の繰り返し)}$

の上に証明図(**)をつなげたものとなります(この書き方はWikipediaを参考にして少し変更したものです)。