MGTPによる記述例


->隔地者である(ラクーン, レッドフォックス, log(隔地者_レッド)).

->隔地者である(レッドフォックス, ラクーン,
   log(隔地者(ラクーン, レッドフォックス))).

->到達する(レッドフォックスの承諾, 電子メール, 7070015, log(到達_レッド)).

->発信される(レッドフォックスの承諾, 電子メール, 7070012, log(発信_レッド)).

->申し込む(ラクーン, レッドフォックス, レッドフォックスへのライセンス,
   log(申込_レッドフォックス)).

->承諾する(レッドフォックス, ラクーン, レッドフォックスの承諾,
   レッドフォックスへのライセンス, log(承諾_レッド)).

->ライセンス(ラクーン, 3000万円, レッドフォックス,
   レッドフォックスへのライセンス, hp制作ソフト,
   log(ライセンス_レッドフォックス)).

申し込む(ラクーン, A, B, C), 承諾する(A, ラクーン, D, B, E)->
   -k(最初に承諾する(A, ラクーン, B, log(事例111の契約不成立(A, B), C, E))),
   -k(defeated(事例111の契約不成立(A, B),
   log(事例111の契約不成立(A, B), C, E))),
   -契約が成立する(B, l(ラクーン, A),
   log(事例111の契約不成立(A, B), C, E));
   k(最初に承諾する(A, ラクーン, B, log(事例111の契約不成立(A, B), C, E)));
   k(defeated(事例111の契約不成立(A, B),
   log(事例111の契約不成立(A, B), C, E))).

承諾する(A, B, C, D, E), 効力が発生する(C, F, G), 承諾する(H, B, I, J, K),
   効力が発生する(I, L, M), {F
   -最初に承諾する(H, B, J,
   log(最初でない承諾(B, A, H, D, J, C, I, F, L), E, G, K, M)).

申し込む(ラクーン, A, B, C), 承諾する(A, ラクーン, D, B, E),
   申し込む(ラクーン, A, B, F), 最初に承諾する(A, ラクーン, B, G),
   ライセンス(ラクーン, 3000万円, A, B, hp制作ソフト, H)->
   -k(最初に承諾する(A, ラクーン, B,
   log(事例111の契約不成立(A, B), C, E))),
   -k(defeated(事例111の契約不成立(A, B),
   log(事例111の契約不成立(A, B), C, E))),
   -k('<'(事例111の契約不成立(A, B), 事例111の契約成立(A, B),
   log(defeated(事例111の契約成立(A, B),
   事例111の契約不成立(A, B)), C, E, F, G, H))),
   defeated(事例111の契約成立(A, B),
   log(defeated(事例111の契約成立(A, B),
   事例111の契約不成立(A, B)), C, E, F, G, H));k(最初に承諾する(A, ラクーン, B,
   log(事例111の契約不成立(A, B), C, E)));
   k(defeated(事例111の契約不成立(A, B),
   log(事例111の契約不成立(A, B), C, E)));
   k('<'(事例111の契約不成立(A, B), 事例111の契約成立(A, B),
   log(defeated(事例111の契約成立(A, B), 事例111の契約不成立(A, B)),
   C, E, F, G, H))).

申し込む(ラクーン, A, B, C), 承諾する(A, ラクーン, D, B, E),
   申し込む(ラクーン, A, B, F), 承諾する(A, ラクーン, G, B, H)->
   -k(defeated(通常の契約成立(ラクーン, A, B),
   log(通常の契約成立(ラクーン, A, B), F, H))),
   -k(最初に承諾する(A, ラクーン, B,
   log(事例111の契約不成立(A, B), C, E))),
   -k('<'(通常の契約成立(ラクーン, A, B), 事例111の契約不成立(A, B),
   log(defeated(事例111の契約不成立(A, B),
   通常の契約成立(ラクーン, A, B)), C, E, F, H))),
   defeated(事例111の契約不成立(A, B),
   log(defeated(事例111の契約不成立(A, B),
   通常の契約成立(ラクーン, A, B)), C, E, F, H));
   k(defeated(通常の契約成立(ラクーン, A, B),
   log(通常の契約成立(ラクーン, A, B), F, H)));
   k(最初に承諾する(A, ラクーン, B,
   log(事例111の契約不成立(A, B), C, E)));
   k('<'(通常の契約成立(ラクーン, A, B), 事例111の契約不成立(A, B),
   log(defeated(事例111の契約不成立(A, B),
   通常の契約成立(ラクーン, A, B)), C, E, F, H))).

申し込む(ラクーン, A, B, C), 承諾する(A, ラクーン, D, B, E),
   申し込む(ラクーン, A, B, F), 最初に承諾する(A, ラクーン, B, G),
   ライセンス(ラクーン, 3000万円, A, B, hp制作ソフト, H)->
   -k(defeated(事例111の契約成立(A, B),
   log(事例111の契約成立(A, B), F, G, H))),
   -k(最初に承諾する(A, ラクーン, B,
   log(事例111の契約不成立(A, B), C, E))),
   -k('<'(事例111の契約成立(A, B), 事例111の契約不成立(A, B),
   log(defeated(事例111の契約不成立(A, B),
   事例111の契約成立(A, B)), C, E, F, G, H))),
   defeated(事例111の契約不成立(A, B),
   log(defeated(事例111の契約不成立(A, B),
   事例111の契約成立(A, B)), C, E, F, G, H));
   k(defeated(事例111の契約成立(A, B),
   log(事例111の契約成立(A, B), F, G, H)));
   k(最初に承諾する(A, ラクーン, B,
   log(事例111の契約不成立(A, B), C, E)));
   k('<'(事例111の契約成立(A, B), 事例111の契約不成立(A, B),
   log(defeated(事例111の契約不成立(A, B),
   事例111の契約成立(A, B)), C, E, F, G, H))).


承諾する(A, B, C, D, E), 効力が発生する(C, F, G), 承諾する(H, B, I, J, K),
   効力が発生する(I, L, M), {F
   -k-(最初に承諾する(H, B, J, log(最初の承諾(B, H, J), O))),
   -k('<'(最初でない承諾(B, A, H, D, J, C, I, F, L), 最初の承諾(B, H, J),
   log(defeated(最初の承諾(B, H, J),
   最初でない承諾(B, A, H, D, J, C, I, F, L)), E, G, K, M, O))),
   defeated(最初の承諾(B, H, J),
   log(defeated(最初の承諾(B, H, J),
   最初でない承諾(B, A, H, D, J, C, I, F, L)), E, G, K, M, O));
   k-(最初に承諾する(H, B, J,
   log(最初の承諾(B, H, J), O)));
   k('<'(最初でない承諾(B, A, H, D, J, C, I, F, L), 最初の承諾(B, H, J),
   log(defeated(最初の承諾(B, H, J),
   最初でない承諾(B, A, H, D, J, C, I, F, L)), E, G, K, M, O))).

申し込む(ラクーン, A, B, C), 承諾する(A, ラクーン, D, B, E),
   申し込む(ラクーン, A, B, F), 承諾する(A, ラクーン, G, B, H)->
   -k(最初に承諾する(A, ラクーン, B,
   log(事例111の契約不成立(A, B), C, E))),
   -k(defeated(事例111の契約不成立(A, B),
   log(事例111の契約不成立(A, B), C, E))),
   -k('<'(事例111の契約不成立(A, B), 通常の契約成立(ラクーン, A, B),
   log(defeated(通常の契約成立(ラクーン, A, B),
   事例111の契約不成立(A, B)), C, E, F, H))),
   defeated(通常の契約成立(ラクーン, A, B),
   log(defeated(通常の契約成立(ラクーン, A, B),
   事例111の契約不成立(A, B)), C, E, F, H));
   k(最初に承諾する(A, ラクーン, B,
   log(事例111の契約不成立(A, B), C, E)));
   k(defeated(事例111の契約不成立(A, B),
   log(事例111の契約不成立(A, B), C, E)));
   k('<'(事例111の契約不成立(A, B), 通常の契約成立(ラクーン, A, B),
   log(defeated(通常の契約成立(ラクーン, A, B),
   事例111の契約不成立(A, B)), C, E, F, H))).

隔地者である(A, B, C), 承諾する(B, A, D, E, F), 発信される(D, G, H, I),
   隔地者である(J, K, L), 意思表示する(K, J, D, M, N),
   到達する(D, O, P, Q), {P != H}->
   -k(defeated(526条1項(A, B, D, H), log(526条1項(A, B, D, H), C, F, I))),
   -k('<'(526条1項(A, B, D, H), 97条1項(J, K, D, P),
   log(defeated(97条1項(J, K, D, P), 526条1項(A, B, D, H)), C, F, I, L, N, Q))),
   defeated(97条1項(J, K, D, P),
   log(defeated(97条1項(J, K, D, P), 526条1項(A, B, D, H)), C, F, I, L, N, Q));
   k(defeated(526条1項(A, B, D, H),
   log(526条1項(A, B, D, H), C, F, I)));
   k('<'(526条1項(A, B, D, H), 97条1項(J, K, D, P),
   log(defeated(97条1項(J, K, D, P), 526条1項(A, B, D, H)), C, F, I, L, N, Q))).

隔地者である(A, B, C), 承諾する(B, A, D, E, F), 到達する(D, 電子メール, G, H),
   隔地者である(I, J, K), 意思表示する(J, I, D, L, M),
   到達する(D, N, O, P), {O != G}->
   -k(defeated(到達主義(A, B, D, G), log(到達主義(A, B, D, G), C, F, H))),
   -k('<'(到達主義(A, B, D, G), 97条1項(I, J, D, O),
   log(defeated(97条1項(I, J, D, O), 到達主義(A, B, D, G)), C, F, H, K, M, P))),
   defeated(97条1項(I, J, D, O),
   log(defeated(97条1項(I, J, D, O), 到達主義(A, B, D, G)), C, F, H, K, M, P));
   k(defeated(到達主義(A, B, D, G),
   log(到達主義(A, B, D, G), C, F, H)));
   k('<'(到達主義(A, B, D, G), 97条1項(I, J, D, O),
   log(defeated(97条1項(I, J, D, O), 到達主義(A, B, D, G)), C, F, H, K, M, P))).

隔地者である(A, B, C), 承諾する(B, A, D, E, F), 発信される(D, G, H, I),
   隔地者である(J, K, L), 意思表示する(K, J, D, M, N),
   到達する(D, O, P, Q), {P != H}->
   -k(defeated(97条1項(J, K, D, P), log(97条1項(J, K, D, P), L, N, Q))),
   -k('<'(97条1項(J, K, D, P), 526条1項(A, B, D, H),
   log(defeated(526条1項(A, B, D, H), 97条1項(J, K, D, P)), C, F, I, L, N, Q))),
   defeated(526条1項(A, B, D, H),
   log(defeated(526条1項(A, B, D, H), 97条1項(J, K, D, P)), C, F, I, L, N, Q));
   k(defeated(97条1項(J, K, D, P),
   log(97条1項(J, K, D, P), L, N, Q)));
   k('<'(97条1項(J, K, D, P), 526条1項(A, B, D, H),
   log(defeated(526条1項(A, B, D, H), 97条1項(J, K, D, P)), C, F, I, L, N, Q))).

隔地者である(A, B, C), 承諾する(B, A, D, E, F), 到達する(D, 電子メール, G, H),
   隔地者である(I, J, K), 承諾する(J, I, D, L, M), 発信される(D, N, O, P), {O != G}->
   -k(defeated(到達主義(A, B, D, G),
   log(到達主義(A, B, D, G), C, F, H))),
-k('<'(到達主義(A, B, D, G), 526条1項(I, J, D, O),
   log(defeated(526条1項(I, J, D, O), 到達主義(A, B, D, G)), C, F, H, K, M, P))),
   defeated(526条1項(I, J, D, O),
   log(defeated(526条1項(I, J, D, O), 到達主義(A, B, D, G)), C, F, H, K, M, P));
   k(defeated(到達主義(A, B, D, G),
   log(到達主義(A, B, D, G), C, F, H)));
   k('<'(到達主義(A, B, D, G), 526条1項(I, J, D, O),
   log(defeated(526条1項(I, J, D, O), 到達主義(A, B, D, G)), C, F, H, K, M, P))).

隔地者である(A, B, C), 承諾する(B, A, D, E, F), 到達する(D, 電子メール, G, H),
   隔地者である(I, J, K), 意思表示する(J, I, D, L, M),
   到達する(D, N, O, P), {O != G}->
   -k(defeated(97条1項(I, J, D, O),
   log(97条1項(I, J, D, O), K, M, P))),
   -k('<'(97条1項(I, J, D, O), 到達主義(A, B, D, G),
   log(defeated(到達主義(A, B, D, G), 97条1項(I, J, D, O)), C, F, H, K, M, P))),
   defeated(到達主義(A, B, D, G),
   log(defeated(到達主義(A, B, D, G), 97条1項(I, J, D, O)), C, F, H, K, M, P));
   k(defeated(97条1項(I, J, D, O),
   log(97条1項(I, J, D, O), K, M, P)));
   k('<'(97条1項(I, J, D, O), 到達主義(A, B, D, G),
   log(defeated(到達主義(A, B, D, G), 97条1項(I, J, D, O)), C, F, H, K, M, P))).

隔地者である(A, B, C), 承諾する(B, A, D, E, F), 到達する(D, 電子メール, G, H),
   隔地者である(I, J, K), 承諾する(J, I, D, L, M), 発信される(D, N, O, P), {O != G}->
   -k(defeated(526条1項(I, J, D, O),
   log(526条1項(I, J, D, O), K, M, P))),
   -k('<'(526条1項(I, J, D, O), 到達主義(A, B, D, G),
   log(defeated(到達主義(A, B, D, G), 526条1項(I, J, D, O)), C, F, H, K, M, P))),
   defeated(到達主義(A, B, D, G),
   log(defeated(到達主義(A, B, D, G), 526条1項(I, J, D, O)), C, F, H, K, M, P));
   k(defeated(526条1項(I, J, D, O),
   log(526条1項(I, J, D, O), K, M, P)));
   k('<'(526条1項(I, J, D, O), 到達主義(A, B, D, G),
   log(defeated(到達主義(A, B, D, G), 526条1項(I, J, D, O)), C, F, H, K, M, P))).


承諾する(A, B, C, D, E), 効力が発生する(C, F, G), 承諾する(H, B, I, J, K),
   効力が発生する(I, L, M), {F
   -k-(最初に承諾する(H, B, J, log(最初の承諾(B, H, J), O))),
   -k('<'(最初の承諾(B, H, J), 最初でない承諾(B, A, H, D, J, C, I, F, L),
   log(defeated(最初でない承諾(B, A, H, D, J, C, I, F, L),
   最初の承諾(B, H, J)), E, G, K, M, O))),
   defeated(最初でない承諾(B, A, H, D, J, C, I, F, L),
   log(defeated(最初でない承諾(B, A, H, D, J, C, I, F, L),
   最初の承諾(B, H, J)), E, G, K, M, O));
   k-(最初に承諾する(H, B, J,
   log(最初の承諾(B, H, J), O)));
   k('<'(最初の承諾(B, H, J),
   最初でない承諾(B, A, H, D, J, C, I, F, L),
   log(defeated(最初でない承諾(B, A, H, D, J, C, I, F, L),
   最初の承諾(B, H, J)), E, G, K, M, O))).


申し込む(A, B, C, D), 承諾する(B, A, E, C, F)->
   -k(defeated(通常の契約成立(A, B, C),
   log(通常の契約成立(A, B, C), D, F))), 契約が成立する(C, l(A, B),
   log(通常の契約成立(A, B, C), D, F));
      k(defeated(通常の契約成立(A, B, C),
   log(通常の契約成立(A, B, C), D, F))).


申し込む(ラクーン, A, B, C), 最初に承諾する(A, ラクーン, B, D),
   ライセンス(ラクーン, 3000万円, A, B, hp制作ソフト, E)->
   -k(defeated(事例111の契約成立(A, B),
   log(事例111の契約成立(A, B), C, D, E))), 契約が成立する(B, l(ラクーン, A),
   log(事例111の契約成立(A, B), C, D, E));
      k(defeated(事例111の契約成立(A, B),
   log(事例111の契約成立(A, B), C, D, E))).


隔地者である(A, B, C), 意思表示する(B, A, D, E, F), 到達する(D, G, H, I)->
   -k(defeated(97条1項(A, B, D, H),
   log(97条1項(A, B, D, H), C, F, I))), 効力が発生する(D, H,
   log(97条1項(A, B, D, H), C, F, I));
      k(defeated(97条1項(A, B, D, H),
   log(97条1項(A, B, D, H), C, F, I))).


隔地者である(A, B, C), 承諾する(B, A, D, E, F), 発信される(D, G, H, I)->
   -k(defeated(526条1項(A, B, D, H),
   log(526条1項(A, B, D, H), C, F, I))), 効力が発生する(D, H,
   log(526条1項(A, B, D, H), C, F, I));
      k(defeated(526条1項(A, B, D, H),
   log(526条1項(A, B, D, H), C, F, I))).

隔地者である(A, B, C), 承諾する(B, A, D, E, F), 到達する(D, 電子メール, G, H)->
   
   -k(defeated(到達主義(A, B, D, G),
   log(到達主義(A, B, D, G), C, F, H))), 効力が発生する(D, G,
   log(到達主義(A, B, D, G), C, F, H));
      k(defeated(到達主義(A, B, D, G),
   log(到達主義(A, B, D, G), C, F, H))).

申し込む(A, B, C, D), 承諾する(B, A, E, C, F)->
   '<'(通常の契約成立(A, B, C), 事例111の契約不成立(B, C),
   log(事例111の契約不成立pr(A, B, C), D, F)).


隔地者である(A, B, C), 承諾する(B, A, D, E, F), 発信される(D, G, H, I), 到達する(D, J, K, L)->
   '<'(97条1項(A, B, D, K), 526条1項(A, B, D, H, K),
   log(526条1項pr(A, B, D, K, H), C, F, I, L)).


隔地者である(A, B, C), 承諾する(B, A, D, E, F), 発信される(D, G, H, I), 到達する(D, J, K, L)->
   '<'(526条1項(A, B, D, H), 到達主義(A, B, D, K, H),
   log(通説pr(A, B, D, H, K), C, F, I, L)).


承諾する(A, B, C, D, E)->
   -k-(最初に承諾する(A, B, D,
   log(最初の承諾(B, A, D), E))), 最初に承諾する(A, B, D,
   log(最初の承諾(B, A, D), E));
   k-(最初に承諾する(A, B, D,
   log(最初の承諾(B, A, D), E))).


承諾する(A, B, C, D, E)->
   意思表示する(A, B, C, D,
   log(意思表示_承諾(B, A, D, C), E)).


「MGTP 上での仮説推論の例」に戻る