Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Thomas Feller, Tim S. Lyon, Piotr Ostropolski-Nalewaja, Sebastian Rudolph

TL;DR

The paper introduces a width-based framework for deciding entailment problems $\textsc{Entailment}(\mathfrak{F},\mathfrak{Q})$ by exploiting countermodels of finite width, with partitionwidth as a central measure. It develops a generic decidability theorem requiring width-controllability and MSO-friendly translations, then specializes to homomorphism-closed queries via finitely universal model sets. The work applies the framework to existential rules, defines the fps (finite partition-width sets) class, and shows how stratification and FO-rewritability shape the landscape of decidable CQ/HUSOMSOQ entailment, including new subclasses and broad applicability to description logics and ontological querying. It also clarifies the relationships among width notions (partitionwidth, treewidth, cliquewidth) and discusses limitations and future directions for width-based decidability beyond universal models. Overall, the results provide a modular toolbox for deriving decidability across expressive logics and query languages, with wide implications for databases, KR, and ontology-based querying.

Abstract

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.

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

TL;DR

The paper introduces a width-based framework for deciding entailment problems by exploiting countermodels of finite width, with partitionwidth as a central measure. It develops a generic decidability theorem requiring width-controllability and MSO-friendly translations, then specializes to homomorphism-closed queries via finitely universal model sets. The work applies the framework to existential rules, defines the fps (finite partition-width sets) class, and shows how stratification and FO-rewritability shape the landscape of decidable CQ/HUSOMSOQ entailment, including new subclasses and broad applicability to description logics and ontological querying. It also clarifies the relationships among width notions (partitionwidth, treewidth, cliquewidth) and discusses limitations and future directions for width-based decidability beyond universal models. Overall, the results provide a modular toolbox for deriving decidability across expressive logics and query languages, with wide implications for databases, KR, and ontology-based querying.

Abstract

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.
Paper Structure (30 sections, 26 theorems, 56 equations, 1 figure, 2 tables)

This paper contains 30 sections, 26 theorems, 56 equations, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Semidecidability via Reduction to FO
  4. Co-Semidecidability via Width Restrictions
  5. The Case of Homomorphism-Closed Queries
  6. Par-ti-tion-width: Definition and Properties
  7. Formal Definition of Par-ti-tion-width of Countable Instances
  8. Partitionwidth and Monadic Second-Order Logic
  9. Robustness under Controlled Modifications
  10. Relationship to Other Width Notions
  11. Application to Existential Rules
  12. Abstracting from Databases: Finite w-Sets
  13. Extending $\mathbf{fps}$ through Stratification
  14. The Case of First-Order Rewritability
  15. The Price of Expressive Querying
  16. ...and 15 more sections

Key Result

Theorem 4.5

Let $\mathsf{w}$ be a width measure, $\mathfrak{F}$ an FO fragment, and $\mathfrak{Q}$ a $\forall$SO fragment such that $\mathfrak{F}$ is $\mathsf{w}$-controllable for $\mathfrak{Q}$. If there exists some fragment $\mathfrak{L}$ such that $\mathsf{w}$ is $\mathfrak{L}$-friendly and the fragment $\{\

Figures (1)

  • Figure 1: Set diagram displaying the inclusions between classes of countable instances satisfying diverse types of width-finiteness, conditioned on signature arity. Example instances witness the strictness of the inclusions ($n$ and $m$ range over $\mathbb{N}$).

Theorems & Definitions (85)

  • Example 1.1
  • proof
  • Definition 4.1: width measures and their properties
  • Definition 4.2: treewidth
  • Definition 4.3: width-based controllability
  • Definition 4.4: effective expressibility
  • Theorem 4.5
  • proof
  • Example 4.6
  • Remark 4.7
  • ...and 75 more