エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を表すことを考えていくブロクです。

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