Download presentation
Presentation is loading. Please wait.
1
導出原理とProlog -論理と形式化 授業資料-
亀山(幸)、2015/6/5, 6/12
2
例1 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
3
例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)
4
例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 もあった!
5
例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
6
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 は同値
7
述語論理の例(本来の導出原理) 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)).
8
述語論理の例(本来の導出原理) [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)))
9
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( , s(0), Z2). by H2 G4 ?- . (ok) by H1 H2 add(s(X),Y,s(Z)) :- add(X, Y, Z).
10
単一化 (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の場合は、一致させる代入のうち、最も制約が少ないもの
11
今日の演習 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の証明図も書きなさい。
12
解答 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つ目と単一化可能なヘッドをもつホーン節がないので失敗。 バックトラックポイントはもうのこっていないので、失敗する。
13
解答 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) バックトラックポイントはもうのこっていないので、失敗する。
Similar presentations
© 2024 slidesplayer.net Inc.
All rights reserved.