論理プログラミング(10) - エレファント・ビジュアライザー調査記録

$n$ のときに成り立つとして $n+1$ のときに成り立つことを証明していきます。

$\mu(d^n(r) \downarrow) \ne \phi$ のときに証明図を書くことができると仮定します。

$n=1$ のときの PLP の正規化された論理式 $d(r)$ は

$\displaystyle unify(q^{(*)}_1 , r^{(*)}) \land p^{(*)}_{11} \land p^{(*)}_{12} \land \cdots \land p^{(*)}_{1l_1}$

$\displaystyle \lor$

$\displaystyle \vdots$

$\displaystyle \lor$

$\displaystyle unify(q^{(*)}_k , r^{(*)}) \land p^{(*)}_{k1} \land p^{(*)}_{k2} \land \cdots \land p^{(*)}_{kl_k}$

という形になります。上についた $(*)$ は変数を何回か置き換えたものであることを表しています。

$d: E \rightarrow E$ は $e \in E$ の各述語式を $d$ で変換したもので置き換えた論理式を正規化したものに写す写像として定義します。

$d^n(r)$ は

$\displaystyle p_{11} \land p_{12} \land \cdots \land p_{1\zeta_1}$

$\displaystyle \lor$

$\displaystyle \vdots$

$\displaystyle \lor$

$\displaystyle p_{\eta 1} \land p_{\eta 2} \land \cdots \land p_{\eta \zeta_\eta}$

という形で、各 $p_{ij}$ は述語式またはunify式となります。

$\sigma(d^{n+1}(r)\downarrow)=true$ となる代入 $\sigma$ をとると $d^{n+1}(r)$ のある連言節を $\sigma$ で写したものはunify式だけからなる連言節 $c$ となります。

$d^{n+1}(r)$ は各 $p_{ij}$ のうちの述語式であるものを $d$ で変換したもので置き換えた論理式を正規化したものなので、 $c$ はある

$\displaystyle \sigma(d(p_{\xi 1} \land p_{\xi 2} \land \cdots \land p_{\xi \zeta_\xi}))$

を正規化したものの一つの連言節となります。

これを $n=1$ のところまで繰り返すと、 $c$ はある

$\displaystyle \sigma(d^n( unify(q^{(*)}_\lambda , r^{(*)}) \land p^{(*)}_{\lambda 1} \land p^{(*)}_{\lambda 2} \land \cdots \land p^{(*)}_{\lambda l_\lambda} )$

を正規化したものの一つの連言節となります。

仮定より各 $\sigma(d^n(p^{(*)}_{\lambda j}))$ を証明する証明図を書くことができるので、その証明図と $n=1$ の証明図を書く議論を組み合わせて、証明図をつなげて、最初に述べた「 $\exists$ 右」をつなげれば $n+1$ のときの証明図を書くことができます。