-
Bag Semantics Query Containment: The CQ vs. UCQ Case and Other Stories
Authors:
Jerzy Marcinkowski,
Piotr Ostropolski-Nalewaja
Abstract:
Query Containment Problem (QCP) is a fundamental decision problem in query processing and optimization. While QCP has for a long time been completely understood for the case of set semantics, decidability of QCP for conjunctive queries under multi-set semantics ($QCP_{\text{CQ}}^{\text{bag}}$) remains one of the most intriguing open problems in database theory. Certain effort has been put, in last…
▽ More
Query Containment Problem (QCP) is a fundamental decision problem in query processing and optimization. While QCP has for a long time been completely understood for the case of set semantics, decidability of QCP for conjunctive queries under multi-set semantics ($QCP_{\text{CQ}}^{\text{bag}}$) remains one of the most intriguing open problems in database theory. Certain effort has been put, in last 30 years, to solve this problem and some decidable special cases of $QCP_{\text{CQ}}^{\text{bag}}$ were identified, as well as some undecidable extensions, including $QCP_{\text{UCQ}}^{\text{bag}}$. In this paper we introduce a new technique which produces, for a given UCQ $Φ$, a CQ $φ$ such that the application of $φ$ to a database $D$ is, in some sense, an approximation of the application of $Φ$ to $D$. Using this technique we could analyze the status of $QCP^{\text{bag}}$ when one of the queries in question is a CQ and the other is a UCQ, and we reached conclusions which surprised us a little bit. We also tried to use this technique to translate the known undecidability proof for $QCP_{\text{UCQ}}^{\text{bag}}$ into a proof of undecidability of $QCP_{\text{CQ}}^{\text{bag}}$. And, as you are going to see, we got stopped just one infinitely small $\varepsilon$ before reaching this ultimate goal.
△ Less
Submitted 1 June, 2025; v1 submitted 10 March, 2025;
originally announced March 2025.
-
Monotone Rewritability and the Analysis of Queries, Views, and Rules
Authors:
Michael Benedikt,
Stanislav Kikot,
Johannes Marti,
Piotr Ostropolski-Nalewaja
Abstract:
We study the interaction of views, queries, and background knowledge in the form of existential rules. The motivating questions concern monotonic determinacy of a query using views w.r.t. rules, which refers to the ability to recover the query answer from the views via a monotone function. We study the decidability of monotonic determinacy, and compare with variations that require the ``recovery f…
▽ More
We study the interaction of views, queries, and background knowledge in the form of existential rules. The motivating questions concern monotonic determinacy of a query using views w.r.t. rules, which refers to the ability to recover the query answer from the views via a monotone function. We study the decidability of monotonic determinacy, and compare with variations that require the ``recovery function'' to be in a well-known monotone query language, such as conjunctive queries or Datalog. Surprisingly, we find that even in the presence of basic existential rules, the borderline between well-behaved and badly-behaved answerability differs radically from the unconstrained case. In order to understand this boundary, we require new results concerning entailment problems involving views and rules.
△ Less
Submitted 20 July, 2024;
originally announced July 2024.
-
The Sticky Path to Expressive Querying: Decidability of Navigational Queries under Existential Rules
Authors:
Piotr Ostropolski-Nalewaja,
Sebastian Rudolph
Abstract:
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 fragmen…
▽ More
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.
△ Less
Submitted 19 July, 2024;
originally announced July 2024.
-
Decidability of Quasi-Dense Modal Logics
Authors:
Piotr Ostropolski-Nalewaja,
Tim S. Lyon
Abstract:
The decidability of axiomatic extensions of the modal logic K with modal reduction principles, i.e. axioms of the form $\Diamond^{k} p \rightarrow \Diamond^{n} p$, has remained a long-standing open problem. In this paper, we make significant progress toward solving this problem and show that decidability holds for a large subclass of these logics, namely, for 'quasi-dense logics.' Such logics are…
▽ More
The decidability of axiomatic extensions of the modal logic K with modal reduction principles, i.e. axioms of the form $\Diamond^{k} p \rightarrow \Diamond^{n} p$, has remained a long-standing open problem. In this paper, we make significant progress toward solving this problem and show that decidability holds for a large subclass of these logics, namely, for 'quasi-dense logics.' Such logics are extensions of K with with modal reduction axioms such that $0 < k < n$ (dubbed 'quasi-density axioms'). To prove decidability, we define novel proof systems for quasi-dense logics consisting of disjunctive existential rules, which are first-order formulae typically used to specify ontologies in the context of database theory. We show that such proof systems can be used to generate proofs and models of modal formulae, and provide an intricate model-theoretic argument showing that such generated models can be encoded as finite objects called 'templates.' By enumerating templates of bound size, we obtain an EXPSPACE decision procedure as a consequence.
△ Less
Submitted 5 June, 2024; v1 submitted 16 May, 2024;
originally announced May 2024.
-
Connecting Proof Theory and Knowledge Representation: Sequent Calculi and the Chase with Existential Rules
Authors:
Tim S. Lyon,
Piotr Ostropolski-Nalewaja
Abstract:
Chase algorithms are indispensable in the domain of knowledge base querying, which enable the extraction of implicit knowledge from a given database via applications of rules from a given ontology. Such algorithms have proved beneficial in identifying logical languages which admit decidable query entailment. Within the discipline of proof theory, sequent calculi have been used to write and design…
▽ More
Chase algorithms are indispensable in the domain of knowledge base querying, which enable the extraction of implicit knowledge from a given database via applications of rules from a given ontology. Such algorithms have proved beneficial in identifying logical languages which admit decidable query entailment. Within the discipline of proof theory, sequent calculi have been used to write and design proof-search algorithms to identify decidable classes of logics. In this paper, we show that the chase mechanism in the context of existential rules is in essence the same as proof-search in an extension of Gentzen's sequent calculus for first-order logic. Moreover, we show that proof-search generates universal models of knowledge bases, a feature also exhibited by the chase. Thus, we formally connect a central tool for establishing decidability proof-theoretically with a central decidability tool in the context of knowledge representation.
△ Less
Submitted 4 June, 2023;
originally announced June 2023.
-
Decidability of Querying First-Order Theories via Countermodels of Finite Width
Authors:
Thomas Feller,
Tim S. Lyon,
Piotr Ostropolski-Nalewaja,
Sebastian Rudolph
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 finit…
▽ More
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.
△ Less
Submitted 21 April, 2025; v1 submitted 13 April, 2023;
originally announced April 2023.
-
Foundations for an Abstract Proof Theory in the Context of Horn Rules
Authors:
Tim S. Lyon,
Piotr Ostropolski-Nalewaja
Abstract:
We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed 'g-sequents,' which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of 'inference ru…
▽ More
We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed 'g-sequents,' which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of 'inference rule types' as sets of operations that act over such objects, and define 'abstract (sequent) calculi' as pairs consisting of a set of g-sequents together with a finite set of operations. Our approach permits an analysis of how certain inference rule types interact in a general setting, demonstrating under what conditions rules of a specific type can be permuted with or simulated by others, and being applicable to any sequent-style proof system that fits within our framework. We then leverage our permutation and simulation results to establish generic calculus and proof transformation algorithms, which show that every abstract calculus can be effectively transformed into a lattice of polynomially equivalent abstract calculi. We determine the complexity of computing this lattice and compute the relative sizes of proofs and sequents within distinct calculi of a lattice. We recognize that top elements in lattices correspond to nested sequent systems, while bottom elements correspond to labeled sequent systems, and observe that top and bottom elements coincide with many known (cut-free) nested and labeled sequent systems for logics characterized by Horn properties.
△ Less
Submitted 12 April, 2023;
originally announced April 2023.
-
Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying
Authors:
Thomas Feller,
Tim S. Lyon,
Piotr Ostropolski-Nalewaja,
Sebastian Rudolph
Abstract:
In our pursuit of generic criteria for decidable ontology-based querying, we introduce 'finite-cliquewidth sets' (FCS) of existential rules, a model-theoretically defined class of rule sets, inspired by the cliquewidth measure from graph theory. By a generic argument, we show that FCS ensures decidability of entailment for a sizable class of queries (dubbed 'DaMSOQs') subsuming conjunctive queries…
▽ More
In our pursuit of generic criteria for decidable ontology-based querying, we introduce 'finite-cliquewidth sets' (FCS) of existential rules, a model-theoretically defined class of rule sets, inspired by the cliquewidth measure from graph theory. By a generic argument, we show that FCS ensures decidability of entailment for a sizable class of queries (dubbed 'DaMSOQs') subsuming conjunctive queries (CQs). The FCS class properly generalizes the class of finite-expansion sets (FES), and for signatures of arity at most 2, the class of bounded-treewidth sets (BTS). For higher arities, BTS is only indirectly subsumed by FCS by means of reification. Despite the generality of FCS, we provide a rule set with decidable CQ entailment (by virtue of first-order-rewritability) that falls outside FCS, thus demonstrating the incomparability of FCS and the class of finite-unification sets (FUS). In spite of this, we show that if we restrict ourselves to single-headed rule sets over signatures of arity at most 2, then FCS subsumes FUS.
△ Less
Submitted 6 September, 2022;
originally announced September 2022.
-
Determinacy of Real Conjunctive Queries. The Boolean Case
Authors:
Jarosław Kwiecień,
Jerzy Marcinkowski,
Piotr Ostropolski-Nalewaja
Abstract:
In their classical 1993 paper [CV93] Chaudhuri and Vardi notice that some fundamental database theory results and techniques fail to survive when we try to see query answers as bags (multisets) of tuples rather than as sets of tuples.
But disappointingly, almost 30 years after [CV93], the bag-semantics based database theory is still in its infancy. We do not even know whether conjunctive query c…
▽ More
In their classical 1993 paper [CV93] Chaudhuri and Vardi notice that some fundamental database theory results and techniques fail to survive when we try to see query answers as bags (multisets) of tuples rather than as sets of tuples.
But disappointingly, almost 30 years after [CV93], the bag-semantics based database theory is still in its infancy. We do not even know whether conjunctive query containment is decidable. And this is not due to lack of interest, but because, in the multiset world, everything suddenly gets discouragingly complicated.
In this paper, we try to re-examine, in the bag semantics scenario, the query determinacy problem, which has recently been intensively studied in the set semantics scenario. We show that query determinacy (under bag semantics) is decidable for boolean conjunctive queries and undecidable for unions of such queries (in contrast to the set semantics scenario, where the UCQ case remains decidable even for unary queries). We also show that -- surprisingly -- for path queries determinacy under bag semantics coincides with determinacy under set semantics (and thus it is decidable).
△ Less
Submitted 23 December, 2021;
originally announced December 2021.
-
A Journey to the Frontiers of Query Rewritability
Authors:
Piotr Ostropolski-Nalewaja,
Jerzy Marcinkowski,
David Carral,
Sebastian Rudolph
Abstract:
This paper is about (first order) query rewritability in the context of theory-mediated query answering. The starting point of our journey is the FUS/FES conjecture, saying that if a theory is core-terminating (FES) and admits query rewriting (BDD, FUS) then it is uniformly bounded. We show that this conjecture is true for a wide class of "local" BDD theories. Then we ask how non-local can a BDD t…
▽ More
This paper is about (first order) query rewritability in the context of theory-mediated query answering. The starting point of our journey is the FUS/FES conjecture, saying that if a theory is core-terminating (FES) and admits query rewriting (BDD, FUS) then it is uniformly bounded. We show that this conjecture is true for a wide class of "local" BDD theories. Then we ask how non-local can a BDD theory actually be and we discover phenomena which we think are quite counter-intuitive.
△ Less
Submitted 3 May, 2021; v1 submitted 21 December, 2020;
originally announced December 2020.
-
On monotonic determinacy and rewritability for recursive queries and views
Authors:
Michael Benedikt,
Stanislav Kikot,
Piotr Ostropolski-Nalewaja,
Miguel Romero
Abstract:
A query Q is monotonically determined over a set of views if Q can be expressed as a monotonic function of the view image. In the case of relational algebra views and queries, monotonic determinacy coincides with rewritability as a union of conjunctive queries, and it is decidable in important special cases, such as for CQ views and queries. We investigate the situation for views and queries in th…
▽ More
A query Q is monotonically determined over a set of views if Q can be expressed as a monotonic function of the view image. In the case of relational algebra views and queries, monotonic determinacy coincides with rewritability as a union of conjunctive queries, and it is decidable in important special cases, such as for CQ views and queries. We investigate the situation for views and queries in the recursive query language Datalog. We give both positive and negative results about the ability to decide monotonic determinacy, and also about the co-incidence of monotonic determinacy with Datalog rewritability.
△ Less
Submitted 12 March, 2020;
originally announced March 2020.
-
The First Order Truth behind Undecidability of Regular Path Queries Determinacy
Authors:
Grzegorz Głuch,
Jerzy Marcinkowski,
Piotr Ostropolski-Nalewaja
Abstract:
In our paper [Głuch, Marcinkowski, Ostropolski-Nalewaja, LICS ACM, 2018] we have solved an old problem stated in [Calvanese, De Giacomo, Lenzerini, Vardi, SPDS ACM, 2000] showing that query determinacy is undecidable for Regular Path Queries. Here a strong generalisation of this result is shown, and -- we think -- a very unexpected one. We prove that no regularity is needed: determinacy remains un…
▽ More
In our paper [Głuch, Marcinkowski, Ostropolski-Nalewaja, LICS ACM, 2018] we have solved an old problem stated in [Calvanese, De Giacomo, Lenzerini, Vardi, SPDS ACM, 2000] showing that query determinacy is undecidable for Regular Path Queries. Here a strong generalisation of this result is shown, and -- we think -- a very unexpected one. We prove that no regularity is needed: determinacy remains undecidable even for finite unions of conjunctive path queries.
△ Less
Submitted 25 January, 2019; v1 submitted 22 August, 2018;
originally announced August 2018.
-
Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable
Authors:
Grzegorz Głuch,
Jerzy Marcinkowski,
Piotr Ostropolski-Nalewaja
Abstract:
For a given set of queries (which are expressions in some query language) $\mathcal{Q}=\{Q_1$, $Q_2, \ldots Q_k\}$ and for another query $Q_0$ we say that $\mathcal{Q}$ determines $Q_0$ if -- informally speaking -- for every database $\mathbb D$, the information contained in the views $\mathcal{Q}({\mathbb D})$ is sufficient to compute $Q_0({\mathbb D})$. Query Determinacy Problem is the problem o…
▽ More
For a given set of queries (which are expressions in some query language) $\mathcal{Q}=\{Q_1$, $Q_2, \ldots Q_k\}$ and for another query $Q_0$ we say that $\mathcal{Q}$ determines $Q_0$ if -- informally speaking -- for every database $\mathbb D$, the information contained in the views $\mathcal{Q}({\mathbb D})$ is sufficient to compute $Q_0({\mathbb D})$. Query Determinacy Problem is the problem of deciding, for given $\mathcal{Q}$ and $Q_0$, whether $\mathcal{Q}$ determines $Q_0$. Many versions of this problem, for different query languages, were studied in database theory. In this paper we solve a problem stated in [CGLV02] and show that Query Determinacy Problem is undecidable for the Regular Path Queries -- the paradigmatic query language of graph databases.
△ Less
Submitted 5 February, 2018;
originally announced February 2018.
-
A Family of Approximation Algorithms for the Maximum Duo-Preservation String Mapping Problem
Authors:
Bartłomiej Dudek,
Paweł Gawrychowski,
Piotr Ostropolski-Nalewaja
Abstract:
In the Maximum Duo-Preservation String Mapping problem we are given two strings and wish to map the letters of the former to the letters of the latter so as to maximise the number of duos. A duo is a pair of consecutive letters that is mapped to a pair of consecutive letters in the same order. This is complementary to the well-studied Minimum Common String Partition problem, where the goal is to p…
▽ More
In the Maximum Duo-Preservation String Mapping problem we are given two strings and wish to map the letters of the former to the letters of the latter so as to maximise the number of duos. A duo is a pair of consecutive letters that is mapped to a pair of consecutive letters in the same order. This is complementary to the well-studied Minimum Common String Partition problem, where the goal is to partition the former string into blocks that can be permuted and concatenated to obtain the latter string.
Maximum Duo-Preservation String Mapping is APX-hard. After a series of improvements, Brubach [WABI 2016] showed a polynomial-time $3.25$-approximation algorithm. Our main contribution is that for any $ε>0$ there exists a polynomial-time $(2+ε)$-approximation algorithm. Similarly to a previous solution by Boria et al. [CPM 2016], our algorithm uses the local search technique. However, this is used only after a certain preliminary greedy procedure, which gives us more structure and makes a more general local search possible. We complement this with a specialised version of the algorithm that achieves $2.67$-approximation in quadratic time.
△ Less
Submitted 30 May, 2017; v1 submitted 8 February, 2017;
originally announced February 2017.
