通过有限宽度的反模型判定一阶理论查询的可判定性
Decidability of Querying First-Order Theories via Countermodels of Finite Width
AI总结：
提出基于有限宽度反模型的通用框架证明逻辑蕴含问题可判定性，采用partitionwidth度量，以存在规则为例展示其涵盖已知可判定类与新规则集，并揭示有限统一集的局限与补救方案。
摘要：
我们提出了一个通用框架，用于证明广泛逻辑蕴含问题（简称查询）的可判定性。该框架基于存在结构简单的反模型，并通过特定类型的宽度度量（以treewidth和cliquewidth为典型示例）来衡量。作为框架的重要特例，我们识别出具有宽度有限且有限通用模型集的逻辑，从而保证广泛的同态封闭查询的可判定性，这涵盖了多种实用的查询语言。作为一种强大的宽度度量，我们建议采用Blumensath的partitionwidth，它包含其他常见的宽度度量，并展现出极具优势的计算与结构特性。以存在规则这一形式化框架为典型示例，我们解释了有限partitionwidth规则集如何包含其他已知的抽象可判定类，并且——利用现有的分层概念——还覆盖了广泛的新规则集。我们揭示了将有限统一集类别纳入该框架的自然局限性，并提出了多种补救方案。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
