Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features

要約

ALC を拡張した記述ロジックにおける充足可能性チェックとクエリの決定可能性に対する非正規パス式の影響を調査します。
私たちが主に興味を持っているオブジェクトは ALCreg と ALCvpl です。これらは、それぞれ通常の言語と目に見えるプッシュダウン言語を使用する with path 式の拡張です。
1 つ目の ALCreg は、Fischer と Ladner のよく知られた命題動的論理の表記上の変形です。
2 番目の ALCvpl は、2007 年に Loding と Serre によって導入および調査されました。ロジック ALCvpl は、既知の決定可能な ALCreg の非正規拡張の多くを一般化します。
一連の決定不可能性の結果を提供します。
まず、ALCvpl の概念充足可能性問題の決定可能性は、一見無害に見える Self 演算子を追加すると失われることを示します。
第二に、公称で拡張された ALCvpl の概念充足可能性問題に対する決定不可能性を確立します。
興味深いことに、私たちの決定不可能性の証明は、単一の非正規 (目に見えるプッシュダウン) 言語、つまり r#s# := { r^n s^n | のみに依存しています。
n in N } は固定ロール名 r および s です。
最後に、古典的なデータベース設定とは対照的に、ALC-TBox の場合にはすでに、r#s# からの非正規アトムを含むクエリに対するクエリ含意の決定不可能性を確立します。

要約(オリジナル)

We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics extending ALC. Our primary objects of interest are ALCreg and ALCvpl, the extensions of with path expressions employing, respectively, regular and visibly-pushdown languages. The first one, ALCreg, is a notational variant of the well-known Propositional Dynamic Logic of Fischer and Ladner. The second one, ALCvpl, was introduced and investigated by Loding and Serre in 2007. The logic ALCvpl generalises many known decidable non-regular extensions of ALCreg. We provide a series of undecidability results. First, we show that decidability of the concept satisfiability problem for ALCvpl is lost upon adding the seemingly innocent Self operator. Second, we establish undecidability for the concept satisfiability problem for ALCvpl extended with nominals. Interestingly, our undecidability proof relies only on one single non-regular (visibly-pushdown) language, namely on r#s# := { r^n s^n | n in N } for fixed role names r and s. Finally, in contrast to the classical database setting, we establish undecidability of query entailment for queries involving non-regular atoms from r#s#, already in the case of ALC-TBoxes.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google