非専門的シンギュラリティー研究所

無限に動き続けるシステムを表す方法を AI なども使って考えていきます。

論理プログラミング(6)

$d' \vdash r'$ 以下( $d' \vdash r'$ から $d' \vdash p''_{ij}$ までの議論)を見てみます。

$d' \vdash r'$ を証明するには

$d' \vdash unify(q''_1, r'')$ 、 $d' \vdash p''_{11}$ 、 $d' \vdash p''_{12}$ 、 $d' \vdash p''_{13}$ 、…のすべてを証明するか、または

$d' \vdash unify(q''_2, r'')$ 、 $d' \vdash p''_{21}$ 、 $d' \vdash p''_{22}$ 、 $d' \vdash p''_{23}$ 、…のすべてを証明するか、または

$d' \vdash unify(q''_3, r'')$ 、 $d' \vdash p''_{31}$ 、 $d' \vdash p''_{32}$ 、 $d' \vdash p''_{33}$ 、…のすべてを証明するか、または…

$d' \vdash unify(q''_k, r'')$ 、 $d' \vdash p''_{k1}$ 、 $d' \vdash p''_{k2}$ 、 $d' \vdash p''_{k3}$ 、…のすべてを証明すれば十分ということがわかります。

ここで $unify(x, y)$ は述語式 $x$ と $y$ が一致するとき真、一致しないとき偽となるもので、述語式として書くこともできます。

これは

$\displaystyle d' \vdash (unify(q''_1, r'') \land p''_{11} \land p''_{12} \land p''_{13} \land \cdots)$

$\displaystyle \lor (unify(q''_2, r'') \land p''_{21} \land p''_{22} \land p''_{23} \land \cdots)$

$\displaystyle \lor (unify(q''_3, r'') \land p''_{31} \land p''_{32} \land p''_{33} \land \cdots)$

$\displaystyle \lor \cdots \lor$

$\displaystyle \lor (unify(q''_k, r'') \land p''_{k1} \land p''_{k2} \land p''_{k3} \land \cdots)$

を証明すれば十分ということがわかります。

言葉で書くとわかりやすく書けそうにないので、次は PLP の数学的定義をして、その後でできればまた説明したいと思います。