Decidability of Querying First-Order Theories via Countermodels of Finite Width

要約

タイトル：有限幅のカウンターモデルを用いた一階理論の問い合わせの決定可能性

要約：
– 広範囲な論理的含意の問い合わせ（クエリ）の決定可能性を確立するための汎用フレームワークを提案する。
– このフレームワークは、特定の幅測定によって評価される構造的に単純なカウンターモデルの存在に基づいており、木幅とクリーク幅が一般的な例として挙げられる。
– 幅収束有限全体モデルセットを示す論理をフレームワークの重要な特殊な場合として特定し、多様な実用的に重要な問い合わせ言語を包含する同型閉じた問い合わせの幅収束有限全体モデルセットに対して決定可能な含意を保証する。
– 特に強力な幅測定として、Blumensathのパーティション幅を提案し、他のよく考慮される幅測定を包含し、非常に有利な計算的および構造的特性を示す。
– 一階ルールの形式論を人気のあるショーケースとして重点的に扱い、既知の抽象的に決定可能なクラスを包含する有限パーティション幅ルールセットと、既存の階層化概念を利用して幅広いルールセットをカバーすることを説明する。
– 有限単一化セットクラスを私たちの枠組みに適合させる自然な制限を示し、その解決策としていくつかのオプションを提供する。

要約(オリジナル)

We propose a generic framework for establishing the decidability of a wide range of logical entailment problems (briefly called querying), based on the existence of countermodels that are structurally simple, gauged by certain types of width measures (with treewidth and cliquewidth as popular examples). As an important special case of our framework, we identify logics exhibiting width-finite finitely universal model sets, warranting decidable entailment for a wide range of homomorphism-closed queries, subsuming a diverse set of practically relevant query languages. As a particularly powerful width measure, we propose Blumensath’s partitionwidth, which subsumes various other commonly considered width measures and exhibits highly favorable computational and structural properties. Focusing on the formalism of existential rules as a popular showcase, we explain how finite partitionwidth sets of rules subsume other known abstract decidable classes but — leveraging existing notions of stratification — also cover a wide range of new rulesets. We expose natural limitations for fitting the class of finite unification sets into our picture and provide several options for remedy.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI