Thomas Feller ; Tim S. Lyon ; Piotr Ostropolski-Nalewaja ; Sebastian Rudolph - Decidability of Querying First-Order Theories via Countermodels of Finite Width

lmcs:11733 - Logical Methods in Computer Science, April 22, 2025, Volume 21, Issue 2 - https://doi.org/10.46298/lmcs-21(2:7)2025
Decidability of Querying First-Order Theories via Countermodels of Finite WidthArticle

Authors: Thomas Feller ; Tim S. Lyon ; Piotr Ostropolski-Nalewaja ; Sebastian Rudolph

    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.


    Volume: Volume 21, Issue 2
    Published on: April 22, 2025
    Accepted on: February 24, 2025
    Submitted on: August 16, 2023
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Artificial Intelligence,Computer Science - Databases,Computer Science - Discrete Mathematics,Mathematics - Logic

    Consultation statistics

    This page has been seen 380 times.
    This article's PDF has been downloaded 165 times.