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

Read original: arXiv:2304.06348 - Published 9/17/2024 by Thomas Feller, Tim S. Lyon, Piotr Ostropolski-Nalewaja, Sebastian Rudolph

🎲

Overview

The paper proposes a general framework for determining the decidability of logical entailment problems, which it refers to as "querying".
The framework is based on the existence of simple, structurally-restricted countermodels, as measured by certain "width" metrics such as treewidth and cliquewidth.
An important special case is logics with width-finite, finitely universal model sets, which allow for decidable entailment for a wide range of homomorphism-closed queries.
The paper introduces partitionwidth as a particularly powerful width measure, which subsumes other common metrics and has favorable computational and structural properties.
Focusing on the formalism of existential rules, the paper shows how finite partitionwidth rule sets can cover a broader range of decidable cases than previous approaches, while also introducing some limitations regarding the class of finite unification sets.

Plain English Explanation

The paper presents a general approach for determining whether certain logical queries are decidable. The key idea is to look at the structure of "countermodels" - models that show a given query is not logically entailed. If these countermodels have a simple, restricted structure that can be captured by certain "width" measures, then the query is likely to be decidable.

As a particularly powerful width measure, the paper introduces partitionwidth, which can subsume other common metrics and has nice computational properties. Applying this to the "existential rules" formalism, the paper shows how partitionwidth can cover a broader range of decidable cases than previous approaches. However, the paper also identifies some limitations regarding a specific class of rule sets called "finite unification sets".

The overall aim is to provide a general, principled way to determine the decidability of logical queries, which is an important problem in areas like knowledge representation and database theory.

Technical Explanation

The paper proposes a generic framework for establishing the decidability of logical entailment problems, which it refers to as "querying". The key idea is to leverage the existence of countermodels that are structurally simple, as measured by certain types of "width" metrics such as treewidth and cliquewidth.

As an important special case, the paper identifies logics that exhibit width-finite, finitely universal model sets. This property allows for decidable entailment for a wide range of homomorphism-closed queries, subsumming many practically-relevant query languages.

A central contribution is the introduction of partitionwidth as a particularly powerful width measure. Partitionwidth subsumes various other commonly-considered width measures and exhibits highly favorable computational and structural properties. Focusing on the formalism of existential rules, the paper shows how finite partitionwidth rule sets can cover a broader range of decidable cases than previously-known abstract decidable classes, while also leveraging notions of stratification.

However, the paper also exposes natural limitations for fitting the class of finite unification sets into this framework, and suggests several options for potential remedies.

Critical Analysis

The paper presents a principled, general framework for establishing the decidability of logical entailment problems, which is an important problem in areas like knowledge representation and database theory. The use of structural restrictions on countermodels, as captured by width measures, is a clever approach that can subsume and generalize previous decidability results.

The introduction of partitionwidth as a powerful width measure is a notable contribution, as it appears to have advantageous computational and structural properties compared to other metrics. Applying this to the existential rules formalism and showing how it can cover a broader range of decidable cases is also a valuable result.

That said, the limitations identified regarding the class of finite unification sets suggest that the framework may not be a complete solution, and further research may be needed to fully resolve the decidability question for this important case. The paper's suggestions for potential remedies are a useful starting point for future work.

Overall, the paper provides a solid foundation for reasoning about the decidability of logical queries, with the potential for significant impact on areas that rely on such reasoning. However, as with any research, there remain open questions and avenues for further exploration.

Conclusion

This paper presents a generic framework for establishing the decidability of logical entailment problems, based on the structural simplicity of countermodels as measured by various width metrics. As a key contribution, it introduces partitionwidth as a powerful width measure with favorable computational properties, and demonstrates how it can be applied to broaden the range of decidable cases in the existential rules formalism.

While the paper identifies limitations regarding the class of finite unification sets, its general approach and the insights around partitionwidth provide a solid foundation for further research into the decidability of logical queries. This work has the potential to significantly impact areas such as knowledge representation and database theory, which rely heavily on reasoning about the decidability of various logical formalisms.

This summary was produced with help from an AI and may contain inaccuracies - check out the links to read the original source documents!

Follow @aimodelsfyi on 𝕏 →

Related Papers

🎲

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

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.

9/17/2024

📈

New!From Width-Based Model Checking to Width-Based Automated Theorem Proving

Mateus de Oliveira Oliveira, Farhad Vadiee

In the field of parameterized complexity theory, the study of graph width measures has been intimately connected with the development of width-based model checking algorithms for combinatorial properties on graphs. In this work, we introduce a general framework to convert a large class of width-based model-checking algorithms into algorithms that can be used to test the validity of graph-theoretic conjectures on classes of graphs of bounded width. Our framework is modular and can be applied with respect to several well-studied width measures for graphs, including treewidth and cliquewidth. As a quantitative application of our framework, we prove analytically that for several long-standing graph-theoretic conjectures, there exists an algorithm that takes a number $k$ as input and correctly determines in time double-exponential in $k^{O(1)}$ whether the conjecture is valid on all graphs of treewidth at most $k$. These upper bounds, which may be regarded as upper-bounds on the size of proofs/disproofs for these conjectures on the class of graphs of treewidth at most $k$, improve significantly on theoretical upper bounds obtained using previously available techniques.

9/17/2024

🤯

Lifted Inference beyond First-Order Logic

Sagar Malhotra, Davide Bizzaro, Luciano Serafini

Weighted First Order Model Counting (WFOMC) is fundamental to probabilistic inference in statistical relational learning models. As WFOMC is known to be intractable in general ($#$P-complete), logical fragments that admit polynomial time WFOMC are of significant interest. Such fragments are called domain liftable. Recent works have shown that the two-variable fragment of first order logic extended with counting quantifiers ($mathrm{C^2}$) is domain-liftable. However, many properties of real-world data, like acyclicity in citation networks and connectivity in social networks, cannot be modeled in $mathrm{C^2}$, or first order logic in general. In this work, we expand the domain liftability of $mathrm{C^2}$ with multiple such properties. We show that any $mathrm{C^2}$ sentence remains domain liftable when one of its relations is restricted to represent a directed acyclic graph, a connected graph, a tree (resp. a directed tree) or a forest (resp. a directed forest). All our results rely on a novel and general methodology of counting by splitting. Besides their application to probabilistic inference, our results provide a general framework for counting combinatorial structures. We expand a vast array of previous results in discrete mathematics literature on directed acyclic graphs, phylogenetic networks, etc.

4/30/2024

The Sticky Path to Expressive Querying: Decidability of Navigational Queries under Existential Rules

Piotr Ostropolski-Nalewaja, Sebastian Rudolph

Extensive research in the field of ontology-based query answering has led to the identification of numerous fragments of existential rules (also known as tuple-generating dependencies) that exhibit decidable answering of atomic and conjunctive queries. Motivated by the increased theoretical and practical interest in navigational queries, this paper considers the question for which of these fragments decidability of querying extends to regular path queries (RPQs). In fact, decidability of RPQs has recently been shown to generally hold for the comprehensive family of all fragments that come with the guarantee of universal models being reasonably well-shaped (that is, being of finite cliquewidth). Yet, for the second major family of fragments, known as finite unification sets (short: fus), which are based on first-order-rewritability, corresponding results have been largely elusive so far. We complete the picture by showing that RPQ answering over arbitrary fus rulesets is undecidable. On the positive side, we establish that the problem is decidable for the prominent fus subclass of sticky rulesets, with the caveat that a very mild extension of the RPQ formalism turns the problem undecidable again.

7/22/2024