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 to employ 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 suggest several options for remedy.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google