導出原理とProlog -論理と形式化 授業資料- 亀山（幸）、2015/6/5, 6/12

例１ H1 P :- Q. H1 Q ⊃ P H2 Q :- R. H2 R ⊃ Q H3 R. H3 R G1 ?- P. H2 H3 G2 ?- Q. R⊃Q R H1 G3 ?- R. Q⊃P Q G4 ?-. (ok) P

例2 H1 Q :- R, S. H1 R∧S ⊃ Q H2 R :- S. H2 S ⊃ R H3 S. H3 S H2 H3 G1 ?- Q. S⊃R S H3 G2 ?- R, S. R S H1 G3 ?- S, S. R∧S⊃Q R∧S G4 ?- S. Q G5 ?- . (ok)

例3-1 H1 P :- Q, R. H1 Q∧R ⊃ P H2 P :- S. H2 S ⊃ P H3 Q :- S. H3 S ⊃ Q G1 ?- P. (fail) S⊃Q S G2 ?- Q, R. Q R H1 G3 ?- S, R. Q∧R⊃P Q∧R G4 ?- R. (fail) P G1に適用可能なのは、H1　だけでなく、H2　もあった！

例3-2 H1 P :- Q, R. H1 Q∧R ⊃ P H2 P :- S. H2 S ⊃ P H3 Q :- S. H3 S ⊃ Q G1 ?- P. G2 ?- S. H2 G3 ?- . (ok) H4 S⊃P S P

Prologの実行の微妙な点 H1 P H1 P. H2 P :- P. H2 P ⊃ P H3 P :- P. H3 P ⊃ P 上にあるホーン節から先に試すので、 ゴール ?- P.　を H1, H2に対して走らせると 止まるが、 H3, H4　に対して走らせると、止まらない。 論理的には、 H1 ∧ H2 と　　H3　∧ H4 は同値

述語論理の例(本来の導出原理） H1 add(0,X, X). H2 add(s(X),Y,s(Z)) :- add(X, Y, Z). ゴール ?- add(s(s(0)), s(0), W). H1 ∀X. add(0, X, X) H2 ∀X,Y,Z. (add(X,Y,Z) ⊃ add(s(X),Y, s(Z))) ゴール ∃W.(add(s(s(0)), s(0), W)).

述語論理の例(本来の導出原理） [Z1:=s(Z2)] [Z2:=s(0)] H2 [X:=0,Y:=s(0),Z:=Z2] H1[X:=s(0)] a(0,s(0),Z2)⊃ a(s(0),s(0),Z1)). H2 [X:=s(0),Y:=s(0),Z:=Z1] a(0,s(0),Z2) a(s(0),s(0),Z1)⊃a(s(s(0)),s(0),W)) a(s(0), s(0), Z1) a(s(s(0)), s(0), W) [W:=s(Z1)] H1 ∀X. (add(0, X, X)) H2 ∀X,Y,Z. (add(X,Y,Z) ⊃ add(s(X),Y,s(Z)))

H2 add(s(X),Y,s(Z)) :- add(X, Y, Z). G1→G2 [X:=s(0),Y:=s(0),Z:=Z1]＋[W:=s(Z1)] 答え W:=s(s(s(0))) G2→G3 [X:=0,Y:=s(0),Z:=Z2]＋[Z1:=s(Z2)] G3→G4 [X:=s(0)]＋[Z2:=s(0)] G1 ?- add(s(s(0)), s(0), W). G2 ?- add( s(0) , s(0), Z1). by H2 G3 ?- add( 0 , s(0), Z2). by H2 G4 ?- . (ok) by H1 H2 add(s(X),Y,s(Z)) :- add(X, Y, Z).

単一化 (unification) add(s(X), Y ,s(Z)) vs add(s(s(0)), s(0), W) 単一化問題： X, Y, Z, W をうまくとることによって、 両者を一致させることができるか？ YES　　[X:=s(0),Y:=s(0),W:=s(Z)] 単一化問題の解： 両者を一致させられるかどうか、と、 YESの場合は、一致させる代入のうち、最も制約が少ないもの

今日の演習 Parent(Alice, Bob). Parent(Alice, Chris). Parent(Chris, Diana). Parent(Eliza, Diana). GP(X, Z) :- Parent(X,Y), Parent(Y,Z). ?- GP(Alice, X). と ?- GP(Eliza, X). を Prolog風に実行する過程を書きなさい。もし余力があれば、得られた解に対応するNKの証明図も書きなさい。

解答 H1 Parent(Alice, Bob). H2 Parent(Alice, Chris). H3 Parent(Chris, Diana). H4 Parent(Eliza, Diana). H5 GP(X, Z) :- Parent(X,Y), Parent(Y,Z). ヘッド ボディ(本体） ?- GP(Eliza, X). H5の変種 H5’ GP(X1,Z1):-P(X1,Y1),P(Y1,Z1). を考え、そのヘッドと単一化 　[X1:=Eliza, Z1:=X]　（あるいは[X1:=Eliza, X:=Z1]と考えてもよい） ?- Parent(Eliza,Y1), Parent(Y1,X). ゴールの1つ目の原子論理式を H4のヘッドと単一化。 　 [Y1:=Diana] ?- Parent(Diana, X). 　ゴールの1つ目と単一化可能なヘッドをもつホーン節がないので失敗。 バックトラックポイントはもうのこっていないので、失敗する。

解答 H1 Parent(Alice, Bob). H2 Parent(Alice, Chris). H3 Parent(Chris, Diana). H4 Parent(Eliza, Diana). H5 GP(X, Z) :- Parent(X,Y), Parent(Y,Z). ヘッド ボディ(本体） ?- GP(Alice, X). H5の変種 H5’ GP(X1,Z1):-P(X1,Y1),P(Y1,Z1). を考え、そのヘッドと単一化 　[X1:=Alice, Z1:=X]　（あるいは[X1:=Alice, X:=Z1]と考えてもよい） ?- Parent(Alice,Y1), Parent(Y1,X). ゴールの1つ目の原子論理式を H1,H2のヘッドと単一化(※）、まずはH1から。 　 [Y1:=Bob] ?- Parent(Bob, X). 　ゴールの1つ目と単一化可能なヘッドをもつホーン節がないので失敗。 　バックトラックポイント※まで戻り、H2のヘッドと単一化。 　　[Y1:=Chris] ?- Parent(Chris,X). ゴールの1つ目とH3のヘッドを単一化。 　　[X:=Diana] ?-. 成功! 　ここまでの代入をまとめると [X:=Diana,X1:=Alice,Y1:=Chris,Z1:=Diana] 　　(next) バックトラックポイントはもうのこっていないので、失敗する。