一句话：提出基于反模型宽度（含 partitionwidth）的通用框架，统一证明广泛逻辑蕴含/查询问题的可判定性。
本文针对逻辑蕴含（查询）问题的可判定性，提出一个通用框架：若某逻辑的查询反模型可按特定宽度度量（树宽、cliquewidth 等）保持结构简单且宽度有限，则其蕴含问题是可判定的。作者引入“宽度有限的有限全域模型集”这一条件，证明它对一大类同态封闭查询保证可判定性，涵盖多种实际查询语言。进一步，作者采用 Blumensath 的 partitionwidth 作为特别有力的宽度度量，它蕴含多种常见宽度概念且具有良好计算与结构性质。以存在规则（existential rules）为主要实例，作者说明有限 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2304-06348,
title = {Decidability of Querying First-Order Theories via Countermodels of Finite Width},
author = {Thomas Feller and Tim S. Lyon and Piotr Ostropolski-Nalewaja and Sebastian Rudolph},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:7)2025}
}