以下の general logic program を考える。
R <- not R.
R <- Q.
P <- not Q.
Q <- not P.
これらのルールは、以下のような MGTP 問題節に変換される。
-> -K R, R ; K R.
Q -> R.
-> -K Q, P ; K Q.
-> -K P, Q ; K P.
上記のルールに対して MGTP 実行を行うと、以下の3つのモデルが生成される。
S1={KR,-KQ,P,KP}
S2={KR,KQ,-KP,Q,R}
S3={KR,KQ,KP}
ここで、S1 と S2 は T-condition を満たさない。よって、 S2 のみが求めるべき安定モデルとなる。
(Inoue, et.al., "Embedding Negation as Failure into a Model Generation Theorem Prover" より)
Lh-Usable(X) <- Person(X), not Ab1(X).
Rh-Usable(X) <- Person(X), not Ab2(X).
Ab1(X) <- -Lh-Usable(X).
Ab2(X) <- -Rh-Usable(X).
Person(john) <-.
-Lh-Usable(john) | -Rh-Usable(john) <- .
この問題においては、john が右利きであるという証拠も左利きであるという 証拠もないが、逆に右利き(左利き)であることを否定する情報もない。 したがって、右利き、左利き両方が安定モデルとなる。
上記のルールを MGTP ルールに変換してモデルを求めると以下の2つとなる。
S1={Person(john),-Lh-Usable(john),Ab1(john),K Ab1(john),-K Ab2(john), Rh-Usable(john)}
S2={Person(john),-Rh-Usable(john),Ab2(john),K Ab2(john),-K Ab1(john), Lh-Usable(john)}
S1、S2はともに T-Condition を満足する。したがって、共に安定モデルである。
MGTP 上での仮説推論の実現の応用として、法的推論への応用が考えられる。 たとえば、以下のような例題を考えてみる。
<例題>
| ラクーン商会は、ソフト販売会社6社に対して、最初に承諾した会社1社 に対して、3000万円のライセンス料でホームページ制作支援ソフトの販売 権をライセンスする旨、契約条項を添付した電子メールを通知し た。ソフト販売会社レッドフォックスは、自社のサーバーのタイムスタンプで 7 月7日午前0時12分にラクーン商会に承諾通知を発信したが、ラクーン商会のサー バーにメールが到着したのは、ラクーン商会のサーバーのタイムスタンプで 午前0時15分であった。 他方、同じくソフト販売会社であるキヌタ堂は、自社のサーバーのタイムスタ ンプで7月 6日午後8時にラクーン商会に承諾通知を発信したが、ラクーン商会 のサーバーにメールが到着したのは、ラクーン商会のサーバーのタイムスタン プで翌日午後4時であった。 いずれの販売会社との契約が成立するか ? |
|---|