Description Logics Go Second-Order — Extending EL with Universally Quantified Concepts

要約

記述ロジックの研究は、歴史的には主に、一次ロジックの決定可能な断片に変換できる機能に焦点を当ててきました。
この論文では、この制限を後に残し、一次論理の外側にある有用で決定可能な拡張を探します。
任意の概念に置き換えることができる変数の形式をとる普遍的に定量化された概念を導入し、この拡張の 2 つのセマンティクスを定義します。
スキーマ セマンティクスでは、概念変数を特定の言語の概念のみで置き換えることができ、様相論理に似た公理スキーマが得られます。
2 次セマンティクスでは、概念変数をドメインの任意のサブセットに置き換えることができます。これは、2 次ロジックの数量化された述語に似ています。
提案されたセマンティクスを研究するために、記述ロジック $\mathcal{EL}$ の拡張に焦点を当てます。
拡張の有用な断片については、さまざまなセマンティクスによってもたらされる結論が一致し、二次セマンティクスに対しても古典的な $\mathcal{EL}$ 推論アルゴリズムを使用できることを示します。
わずかに小さいが依然として有用なフラグメントについては、拡張の多項式決定可能性を示すこともできました。
特に、このフラグメントは、追加のコンストラクターを必要とせずに、一般化された形式の役割チェーン公理、積極的自己制限、および KL-ONE の (ローカル) 役割値マップのいくつかの形式を表現できます。

要約(オリジナル)

The study of Description Logics have been historically mostly focused on features that can be translated to decidable fragments of first-order logic. In this paper, we leave this restriction behind and look for useful and decidable extensions outside first-order logic. We introduce universally quantified concepts, which take the form of variables that can be replaced with arbitrary concepts, and define two semantics of this extension. A schema semantics allows replacements of concept variables only by concepts from a particular language, giving us axiom schemata similar to modal logics. A second-order semantics allows replacement of concept variables with arbitrary subsets of the domain, which is similar to quantified predicates in second-order logic. To study the proposed semantics, we focus on the extension of the description logic $\mathcal{EL}$. We show that for a useful fragment of the extension, the conclusions entailed by the different semantics coincide, allowing us to use classical $\mathcal{EL}$ reasoning algorithms even for the second-order semantics. For a slightly smaller, but still useful, fragment, we were also able to show polynomial decidability of the extension. This fragment, in particular, can express a generalized form of role chain axioms, positive self restrictions, and some forms of (local) role-value-maps from KL-ONE, without requiring any additional constructors.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google