導出原理とProlog -論理と形式化授業資料-

導出原理とProlog
-論理と形式化授業資料亀山（幸）、2015/6/5, 6/12
例１
H1 P :- Q.
H2 Q :- R.
H3 R.
G1
G2
G3
G4
?- P.
?- Q.
?- R.
?-. (ok)
H1 Q ⊃ P
H2 R ⊃ Q
H3 R
H1
Q⊃P
H2 H3
R⊃Q R
Q
P
例2
H1 Q :- R, S.
H2 R :- S.
H3 S.
G1
G2
G3
G4
G5
?- Q.
?- R, S.
?- S, S.
?- S.
?- . (ok)
H1 R∧S ⊃ Q
H2 S ⊃ R
H3 S
H2 H3
H3
S⊃R S
S
R
H1
R∧S
R∧S⊃Q
Q
例3-1
H1
H2
H3
H4
P :- Q, R.
P :- S.
Q :- S.
S.
G1 ?- P.
G2 ?- Q, R.
G3 ?- S, R.
G4 ?- R.
(fail)
H1
H2
H3
H4
Q∧R ⊃ P
S⊃P
S⊃Q
S
H3 H4
S⊃Q S (fail)
R
Q
H1
Q∧R
Q∧R⊃P
P
G1に適用可能なのは、H1 だけでなく、H2 もあった！
例3-2
H1
H2
H3
H4
P :- Q, R.
P :- S.
Q :- S.
S.
G1 ?- P.
G2 ?- S.
G3 ?- . (ok)
H1
H2
H3
H4
Q∧R ⊃ P
S⊃P
S⊃Q
S
H2
S⊃P
H4
S
P
Prologの実行の微妙な点
H1 P.
H2 P :- P.
H1 P
H2 P ⊃ P
H3 P :- P.
H4 P.
H3 P ⊃ P
H4 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)⊃
H2 [X:=s(0),Y:=s(0),Z:=Z1]
a(s(0),s(0),Z1)). a(0,s(0),Z2)
a(s(0), s(0), Z1)
a(s(0),s(0),Z1)⊃a(s(s(0)),s(0),W))
[W:=s(Z1)]
a(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)))
G1→G2 [X:=s(0),Y:=s(0),Z:=Z1]＋[W:=s(Z1)]
G2→G3 [X:=0,Y:=s(0),Z:=Z2]＋[Z1:=s(Z2)] 答え
W:=s(s(s(0)))
G3→G4 [X:=s(0)]＋[Z2:=s(0)]
G1
G2
G3
G4
?- add(s(s(0)), s(0), W).
?- add( s(0) , s(0), Z1).
?- add( 0 , s(0), Z2).
?- . (ok)
by H2
by H2
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
H2
H3
H4
H5
Parent(Alice, Bob).
ヘッド
Parent(Alice, Chris).
Parent(Chris, Diana).
Parent(Eliza, Diana).
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
H2
H3
H4
H5
Parent(Alice, Bob).
ヘッド
Parent(Alice, Chris).
Parent(Chris, Diana).
Parent(Eliza, Diana).
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)
バックトラックポイントはもうのこっていないので、失敗する。

Download Report