エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

論理プログラミング(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 の数学的定義をして、その後でできればまた説明したいと思います。