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

arXiv: https://arxiv.org/abs/2304.06348 · HTML: https://mlsanity.com/paper/2304.06348/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 85 references that are in the map.
- First posted on arXiv 13 Apr 2023.

## Builds on (most cited first, 11 of 11)

- [Ontology-based Data Access: A Study through Disjunctive Datalog, CSP, and MMSNP](https://mlsanity.com/paper/1301.6479/) (2013)
- [Acyclicity Notions for Existential Rules and Their Application to Query Answering in Ontologies](https://mlsanity.com/paper/1406.4110/) (2014)
- [Querying the Guarded Fragment](https://mlsanity.com/paper/1309.5822/) (2013)
- [Unary negation](https://mlsanity.com/paper/1309.2069/) (2013)
- [Rewritability in Monadic Disjunctive Datalog, MMSNP, and Expressive Description Logics](https://mlsanity.com/paper/1701.02231/) (2017)
- [Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying](https://mlsanity.com/paper/2209.02464/) (2022)
- [Combining Existential Rules and Transitivity: Next Steps](https://mlsanity.com/paper/1504.07443/) (2015)
- [Finite Model Theory of the Triguarded Fragment and Related Logics](https://mlsanity.com/paper/2101.08377/) (2021)
- [Capturing Homomorphism-Closed Decidable Queries with Existential Rules](https://mlsanity.com/paper/2107.07811/) (2021)
- [Nominals, Inverses, Counting, and Conjunctive Queries or: Why Infinity is your Friend!](https://mlsanity.com/paper/1401.3849/) (2014)
- [On the BDD/FC Conjecture](https://mlsanity.com/paper/1408.2081/) (2014)

## Abstract (arXiv)

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.