拡張論理型言語による記述例
(% で始まる行はコメント)。
ゴールの記述
ラクーン商会との契約が成立することを証明するためのゴール :
契約が成立する(agt=レッドフォックスへのライセンス,basis=l(ラクーン,レッドフォックス)).
% 契約の成立条件
通常の契約成立(X,Y,I)::
契約が成立する(agt=I, basis=l(X,Y))<=
申し込む(agt=X, goal=Y, obj=I),
承諾する(agt=Y, goal=X, obj=I).
事例111の契約成立(Y,I)::
契約が成立する(agt=I, basis=l(ラクーン,Y))<=
申し込む(agt=ラクーン, goal=Y, obj=I),
最初に承諾する(agt=Y, goal=ラクーン, obj=I),
ライセンス(agt=ラクーン, goal=Y, obj=hp制作ソフト, condition=3000万円, id=I).
事例111の契約不成立(Y,I)::
-契約が成立する(agt=I, basis=l(ラクーン,Y))<=
申し込む(agt=ラクーン, goal=Y, obj=I),
承諾する(agt=Y, goal=ラクーン, obj=I),
not 最初に承諾する(agt=Y, goal=ラクーン, obj=I).
事例111の契約不成立pr(X,Y,I)::
通常の契約成立(X,Y,I)<事例111の契約不成立(Y,I)<-
申し込む(agt=X, goal=Y, obj=I),
承諾する(agt=Y, goal=X, obj=I).
最初の承諾(X,Y,I)::
最初に承諾する(agt=Y, goal=X, obj=I)<-
承諾する(agt=Y, goal=X, obj=I),
not -最初に承諾する(agt=Y, goal=X, obj=I).
最初でない承諾(X,Y1,Y2,I1,I2,ID1,ID2,T1,T2)::
-最初に承諾する(agt=Y2, goal=X, obj=I2)<-
承諾する(agt=Y1, goal=X, obj=I1, id=ID1),
効力が発生する(agt=ID1, time=T1),
承諾する(agt=Y2, goal=X, obj=I2, id=ID2),
効力が発生する(agt=ID2, time=T2),
{T1
%% 民法
97条1項(X,Y,I,T)::
効力が発生する(agt=I, time=T)<=
隔地者である(agt=X, basis=Y),
意思表示する(agt=Y, goal=X, id=I),
到達する(agt=I, time=T).
意思表示_承諾(X,Y,I,ID)::
意思表示する(agt=Y, goal=X, obj=I, id=ID)<-
承諾する(agt=Y, goal=X, obj=I, id=ID).
%隔地者(X,Y)::
%隔地者である(agt=X, basis=Y)<-隔地者である(agt=Y, basis=X).
526条1項(X,Y,I,T)::
効力が発生する(agt=I, time=T)<=
隔地者である(agt=X, basis=Y),
承諾する(agt=Y, goal=X, id=I),
発信される(agt=I, time=T).
526条1項pr(X,Y,I,T1,T2)::
97条1項(X,Y,I,T1)<526条1項(X,Y,I,T2,T1)<-
隔地者である(agt=X, basis=Y),
承諾する(agt=Y, goal=X, id=I),
発信される(agt=I, time=T2),
到達する(agt=I, time=T1).
%% 学説
到達主義(X,Y,I,T)::
効力が発生する(agt=I, time=T)<=
隔地者である(agt=X, basis=Y),
承諾する(agt=Y, goal=X, id=I),
到達する(agt=I, time=T, implement=電子メール).
通説pr(X,Y,I,T1,T2)::
526条1項(X,Y,I,T1)<到達主義(X,Y,I,T2,T1)<-
隔地者である(agt=X, basis=Y),
承諾する(agt=Y, goal=X, id=I),
発信される(agt=I, time=T1),
到達する(agt=I, time=T2).
%% 無矛盾性制約
ic(I,T1,T2):: <- 効力が発生する(agt=I, time=T1),
効力が発生する(agt=I, time=T2),
{T1!=T2}.
% {equal(T1,T2)==false}.
%% 事実関係
申込_レッドフォックス::
申し込む(agt=ラクーン, goal=レッドフォックス,
obj=レッドフォックスへのライセンス)<-- .
ライセンス_レッドフォックス::
ライセンス(agt=ラクーン, goal=レッドフォックス, obj=hp制作ソフト,
condition=3000万円, id=レッドフォックスへのライセンス)<-- .
承諾_レッド::
承諾する(agt=レッドフォックス, goal=ラクーン,
obj=レッドフォックスへのライセンス, id=レッドフォックスの承諾)<-- .
発信_レッド::
発信される(agt=レッドフォックスの承諾, time=7070012, implement=電子メール)<-- .
到達_レッド::
到達する(agt=レッドフォックスの承諾, time=7070015, implement=電子メール)<-- .
隔地者_レッド1::
隔地者である(agt=ラクーン, basis=レッドフォックス)<-- .
隔地者_レッド2::
隔地者である(agt=レッドフォックス, basis=ラクーン)<-- .
申込_キヌタ::
申し込む(agt=ラクーン, goal=キヌタ, obj=キヌタへのライセンス)<-- .
ライセンス_キヌタ::
ライセンス(agt=ラクーン, goal=キヌタ, obj=hp制作ソフト, condition=3000万円,
id=キヌタへのライセンス)<-- .
承諾_キヌタ::
承諾する(agt=キヌタ, goal=ラクーン, obj=キヌタへのライセンス,
id=キヌタの承諾)<-- .
発信_キヌタ::
発信される(agt=キヌタの承諾, time=7062000, implement=電子メール)<-- .
到達_キヌタ::
到達する(agt=キヌタの承諾, time=7071600, implement=電子メール)<-- .
隔地者_キヌタ1::
隔地者である(agt=ラクーン, basis=キヌタ)<-- .
隔地者_キヌタ2::
隔地者である(agt=キヌタ, basis=ラクーン)<-- .
「MGTP 上での仮説推論の例」に戻る