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.
翻译:我们提出了一种通用框架,用于建立广泛逻辑蕴含问题(简称查询)的可判定性。该框架基于存在结构简单的反模型,这些反模型通过特定类型的宽度度量(以树宽和团宽为典型例子)来衡量。作为该框架的一个重要特例,我们识别出具有宽度有限且有限通用模型集的逻辑系统,这保证了对于广泛同态封闭查询(涵盖多种实际相关的查询语言)的可判定蕴含关系。作为特别强大的宽度度量,我们引入了Blumensath划分宽度概念,该度量不仅涵盖了其他常见的宽度度量,还展现出高度有利的计算与结构特性。以存在规则形式化方法为典型示例,我们阐释了有限划分宽度规则集如何包含其他已知抽象可判定类,同时利用现有分层概念覆盖大量新型规则集。本文揭示了有限合一集类适配该框架的内在局限性,并提供了多种解决方案。