Strong Equivalence in Answer Set Programming with Constraints

要約

制約を備えた回答セットプログラミングの拡張フレームワーク内の強力な同等性の概念を調査します。
2つのグループのルールは、非公式に言えば、どんなコンテキストでも同じ意味を持っている場合、強く同等であると見なされます。
特定の仮定の下で、この拡張設定のルールセット間の強い等価性は、制約との論理におけるそれらの同等性によって正確に特徴付けられることを実証します。
さらに、制約を備えた言語への制約を処理するいくつかのクリンゴベースの回答セットソルバーの言語からの翻訳を提示します。
この翻訳により、これらのソルバーのコンテキスト内での強い等価性について、こことここの論理を活用することができます。
また、このコンテキストで強力な等価性を決定するという計算の複雑さを探ります。

要約(オリジナル)

We investigate the concept of strong equivalence within the extended framework of Answer Set Programming with constraints. Two groups of rules are considered strongly equivalent if, informally speaking, they have the same meaning in any context. We demonstrate that, under certain assumptions, strong equivalence between rule sets in this extended setting can be precisely characterized by their equivalence in the logic of Here-and-There with constraints. Furthermore, we present a translation from the language of several clingo-based answer set solvers that handle constraints into the language of Here-and-There with constraints. This translation enables us to leverage the logic of Here-and-There to reason about strong equivalence within the context of these solvers. We also explore the computational complexity of determining strong equivalence in this context.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google