PelletとHermiTを用いたProtegeのユニバーサル定量化の理解

Question

私はProtétéを初めて使用しているので、私は非常に基本的な質問があります。 私はクラスChildとParentを持っています。 ChildのサブクラスはGirlです。

child1はchild2はChildとannaとpeterが持っているタイプの両方のタイプParentがあり、タイプGirlを持っています。さらに、anna isParentOf child1とpeter isParentOf child2の関係があり、それ以上の特性はありません。

今度はParentOfGirlというクラスをParent and isParentOf only Girlに相当するように定義します。私は推論家がこの新しいタイプを持っていると推測することを期待しますが、それはありません。anna

Inverse functionalプロパティをisParentOfに追加しました。これは、親が複数の子を持つことができるためです。私が関係にSymmetricを追加すると、annaのタイプはParentOfGirlになりますが、isParentOfを対称にすることは望ましくありません。

私は対称性のない上記のセマンティクスを見れば、私はこれを参照してください。

ParentOfGirl≡{アンナ、ピーター} {⋂のxεフクロウ：シング|もし∀y（x、y）はεisParentOf次いでYεガール}

child1ののε子とchild1のεガール

isParentOf≡{（アンナ、child1の）、（ピーター、child2の）}

はannaに関連するタイプChildの唯一の個人であり、Girlタイプもあります。この場合、推論者は右から左への関係だけを見ることができます。isParentOfが対称であれば、それはannaであることが推測されるからです。さらに、peterは、お子様2との関係になかった場合はParentOfGirlにもなると思います。しかし、これも起こりません。

なぜ、推論（PelletまたはHermiT）ではannaがParentOfGirlであると表示されませんか。

Answer 1

@AKSWはコメントに間違いがありません。推論家は、親が女性の子供しか持たないかどうかは分かりません。たとえば、個人にタイプを追加するなどして、この機能をアサーションする必要があります。

この場合、このアサーションはあなたが求める推論と同等ですが、実際には良い回避策ではありません。

forallを一部に変更すると、少なくとも1人の少女の親を見つけることができます。これはあなたのターゲットクラスのスーパークラスであり、アプリケーションの実行に役立ちます。