Source-linked AI summary
Querying the Guarded Fragment
Vince Bárány, Georg Gottlob, Martin Otto
TL;DR
For guarded theories and unions of conjunctive queries, finite-model entailment and bounds on finite models are central questions. The paper uses guarded-cover techniques to establish finite controllability and gives finite-model size bounds for guarded fragments.
Problem
Little was known about the size of the smallest finite models of satisfiable guarded sentences, while recursive bounds on countermodels would yield decidability of query answering.
Source: §1.1 · p. 2Method
The approach reduces GF/UCQ entailment to an equivalent entailment involving χq and uses Rosati covers, alongside construction of weakly N-acyclic, N-conformal hypergraph covers.
Source: §1.3 · p. 5Results
For GF and CGF, UCQ entailment over all models equals finite-model entailment, and satisfiable CGF formulas have models exponential in length and doubly exponential in width.
Source: §1.3 · p. 6Takeaways & Limitations
For fixed width and N, the constructed covers are computable in polynomial time and are conformal when N exceeds the width.
Source: §1.3 · p. 5The bounds for query answering over models of fixed guarded sentences are not all tight.
Source: §1.3 · p. 7
Abstract
from arXiv · showhide
Evaluating a Boolean conjunctive query Q against a guarded first-order theory F is equivalent to checking whether "F and not Q" is unsatisfiable. This problem is relevant to the areas of database theory and description logic. Since Q may not be guarded, well known results about the decidability, complexity, and finite-model property of the guarded fragment do not obviously carry over to conjunctive query answering over guarded theories, and had been left open in general. By investigating finite guarded bisimilar covers of hypergraphs and relational structures, and by substantially generalising Rosati's finite chase, we prove for guarded theories F and (unions of) conjunctive queries Q that (i) Q is true in each model of F iff Q is true in each finite model of F and (ii) determining whether F implies Q is 2EXPTIME-complete. We further show the following results: (iii) the existence of polynomial-size conformal covers of arbitrary hypergraphs; (iv) a new proof of the finite model property of the clique-guarded fragment; (v) the small model property of the guarded fragment with optimal bounds; (vi) a polynomial-time solution to the canonisation problem modulo guarded bisimulation, which yields (vii) a capturing result for guarded bisimulation invariant PTIME.
1. Introduction
The paper studies whether conjunctive-query answering over guarded theories retains finite-model guarantees, even though queries need not be guarded. It answers this and related questions about complexity, model sizes, covers, and canonisation.
1.3. Summary of results.
- For every guarded-fragment sentence ϕ and UCQ q, entailment over all models is equivalent to entailment over finite models.If ϕ ∧¬q is satisfiable, the paper also gives a finite-model size bound.Source: §1.3 · pp. 5–6
1.2. Applications to databases and description logic.
- The paper extends finite controllability to query answering under GTGD and WGTGD theories.Weakly guarded TGD theories can be translated into guarded TGD theories for this purpose.Source: §1.3 · p. 5, §1.2 · p. 5
1.3. Summary of results.
- For N ≥2, the Rosati cover construction yields weakly N-acyclic hypergraph covers, computable in polynomial time for fixed width and N.These covers support the reduction from query answering to acyclic queries and enable finite controllability.Source: §1.3 · pp. 5–6
- Every hypergraph has a conformal cover, and the construction gives polynomial-size covers when width is bounded.The stated size bound is |H|wO(w).Source: §1.3 · p. 6
- For clique-guarded formulas, UCQ entailment is finitely controllable, yielding a new proof of the fragment’s finite-model property.When ϕ ∧¬q is satisfiable, it has a finite model with the stated size bound.Source: §1.3 · p. 6
- Every satisfiable CGF formula, and thus every satisfiable GF formula, has a finite model exponential in length and doubly exponential in width.For every k ≥2, the k-variable fragment has finite models exponential in formula length.Source: §1.3 · p. 6
- UCQ answering over guarded theories is 2EXPTIME-complete; acyclic UCQs admit ExpTime-complete answering, while some fixed-theory bounds remain untight.BCQ answering remains 2EXPTIME-complete even for bounded arity.Source: §1.3 · p. 7
- A polynomial-time canonisation procedure captures the PTIME Boolean queries invariant under guarded bisimulation.The procedure reconstructs a representative from the invariant that characterises the guarded-bisimulation class.Source: §1.3 · p. 7
2. Hypergraphs and guarded fragments
This section establishes the guarded-fragment and hypergraph notions used in the paper, then develops weakly acyclic covers and query treeification as tools for reasoning about guarded theories and conjunctive queries.
2.1. Guarded fragments.
- GF restricts quantification to guards covering the quantified variables, while CGF allows clique-guarded tuples; GF formulas are invariant under guarded bisimulation.Source: §2.1 · pp. 8–9
2. Hypergraphs and guarded fragments
- Structures correspond to hypergraphs of maximal guarded sets; for finite hypergraphs, acyclicity combines chordality and conformality and is equivalent to tree decomposability.Source: §2.2 · p. 10
2.2. Hypergraphs, acyclicity and covers.
- A weakly N-acyclic cover makes every homomorphism from a structure of size at most N factor through a guarded tree-decomposable structure mapping to the original.Source: §2.2 · p. 11
2.3. Conjunctive queries.
- For guarded theories, q and its treeification χτq have equivalent entailment; χτq is an ACQ interpolant, and the interpolation property also holds over finite models.The paper identifies ACQs with the intersection of GF and UCQ.Source: §2.3 · p. 11, An interpolation property · p. 13
- Treeification χτq is constructible in time |q|r^O(h)(hw)^O(hw), where h is query height and w is signature width.Source: §2.3 · p. 11
- For fixed signatures, treeifications have size h^O(h), with a 2^Ω(h) lower bound even without redundant disjuncts.Source: §2.3 · p. 12
3. The Rosati cover
This section adapts Rosati’s finite-chase construction into a guarded-bisimilar cover, combining conformality, weak acyclicity, and controlled size, with a simpler proof of faithfulness for bounded-size conjunctive queries. It establishes distinctness along bounded predecessor chains, N-conformality of R_N, and guarded tree-decomposable substructures containing specified projected images.
3. The Rosati cover
- For every N ≥ 2, the construction gives N-conformal hypergraphs RN whose squares are weakly N-acyclic covers, with size |I|wO(N) and polynomial-time construction for fixed width and N.The analogous result holds for guarded-bisimulation invariants of finite relational structures and guarded-bisimilar covers.Source: §3 · p. 13
- Distinguishing each guarded tuple yields a weakly N-acyclic guarded-bisimilar cover of A of size |A|wO(N²); when N > w, Rw+1 is a conformal cover.Here w is the width of A.Source: §3 · p. 13
3.1. The definition of RN.
- RN uses terms of height at most N to realize the invariant’s guarded-bisimulation types, and truncation yields a chain of covers inducing guarded bisimulations.The constructed cover has guarded-bisimulation invariant I.Source: §3.1 · pp. 14–16
3.2. Size of the Rosati cover.
- For m = N², the number of terms in RN is bounded by |I|wO(N).The bound follows by counting the signature symbols and bounding the symbols in each term of height at most N.Source: §3.2 · p. 17
3.3. Auxiliary notions. ρ(
- The auxiliary sibling and predecessor relations partition guarded pairs; ≡ has guarded equivalence classes, while ≺ has no directed cycles of length ≤ N and is transitive on guarded sets for m ≥ N ≥ 3.The section also establishes compatibility properties between ≡ and ≺ and a condition on ≺-maximal elements of primary guards.Source: §3.3 · p. 17
- Every predecessor chain of length at most N consists of pairwise distinct terms.Source: §3.3 · p. 17
3.4. N-conformality of RN.
- In R_N, whenever every pair in a clique of at most N terms is guarded, the entire clique is guarded.Proposition 3.7 establishes this N-conformality property.Source: §3.4 · p. 18
3.5. Weak N-acyclicity of RN2 over RN.
- For M=(N^2+N)/2 ≤ m, every homomorphism h:S→R_m^N has its π∘h-image inside a guarded tree-decomposable substructure of R_m^N.The substructure need not be induced.Source: §3.5 · p. 19
- The construction adds chords iteratively and stabilizes within N(N−1)/2 steps, yielding an acyclic substructure containing the image.It uses N-conformality to obtain the acyclic substructure after the resulting Gaifman graph is chordal.Source: §3.5 · p. 20
4. Finite controllability and small models
The section establishes finite controllability and finite-model size bounds for guarded-fragment query answering, then extends these results to the clique-guarded fragment. The extension uses a translation to guarded sentences and yields finite controllability and corresponding bounds for clique-guarded theories.
4. Finite controllability and small models
- Guarded-theory UCQ answering is finitely controllable: ϕ |= q iff ϕ |=fin q, with finite countermodel bounds in terms of query height and signature width.The section also reports optimal upper bounds for the relevant smallest finite models.Source: §4 · pp. 20–21
- Every satisfiable sentence of the k-variable guarded fragment has finite models exponential in the formula length.Source: §4 · p. 21
- If a guarded sentence has a model in C_F, it also has one of size 2^O(|ϕ|).C_F is the class of structures with no homomorphic image of any member of F.Source: §4 · p. 21
- Uniform interpolation for the guarded fragment and positive existential fragment also holds under finite-model semantics.Source: §4 · p. 21
4.1. Finite controllability for the clique-guarded fragment.
- A translation from clique-guarded to guarded sentences extends the finite-controllability reduction from satisfiability to query entailment.The reduction is adapted to keep formula-size blow-up small.Source: §4 · p. 21, §4.1 · p. 22
- Clique-guarded UCQ answering is finitely controllable, and satisfiable ϕ ∧ ¬q has a finite model bounded by query height and signature width.Source: §4.1 · p. 23
5. Complexity of query answering
The section establishes the complexity of query answering over guarded theories and shows how it changes under restrictions on queries, theories, and input structures. It also gives reductions explaining several hardness results.
5. Complexity of query answering
- When the signature width is bounded, query answering has a matching double-exponential lower bound; for fixed signatures, the section gives a single-exponential lower bound.The lower bounds are stated alongside the corresponding restricted-signature time bounds.Source: §5 · p. 23
- For acyclic unions of conjunctive queries, answering against any guarded sentence is in ExpTime, and is ExpTime-complete for certain fixed sentences.The reduction to guarded-fragment satisfiability avoids the exponential blow-up incurred by treeification.Source: §5 · p. 24
- 2ExpTime-completeness holds for guarded-theory query answering, even with a fixed query.The section also gives a time bound whose double-exponential dependence is on query height and signature width.Source: §5 · pp. 23–24
- A fixed guarded sentence can make answering acyclic unions of conjunctive queries ExpTime-hard.The reduction encodes alternating polynomial-space computation using models that represent computation trees and queries that detect errors in the encoding.Source: §5 · pp. 24–25
- For bounded-width input conjunctions, answering a BCQ against a guarded sentence with constants is PSpace-hard.The reduction uses Boolean valuation trees and a query that detects a clause falsified by an assignment.Source: §5 · pp. 27–28
- With a fixed universal guarded sentence, answering a BCQ from an input conjunction of atoms is ΠP2-complete.The hardness proof reduces quantified propositional formula validity to query answering.Source: §5 · pp. 28–29
- For fixed guarded sentences and fixed input queries, data complexity is co-NP, and is co-NP-complete already for the query ⊥ and certain universal sentences.For fixed guarded sentences, satisfiability of an input conjunction is in NP and is NP-complete for certain universal sentences.Source: §5 · p. 29
- For a fixed universal guarded sentence, deciding whether an input conjunction is satisfiable is NP-complete for certain sentences.The hardness result encodes graph 3-colourability as satisfiability of the input conjunction together with a fixed sentence.Source: §5 · p. 29
6. Canonisation and capturing
The section constructs a polynomial-time canonisation for guarded bisimulation and uses it to capture guarded-bisimulation-invariant polynomial time. The construction orders a complete invariant and inverts it to obtain canonical representatives.
6. Canonisation and capturing
- Guarded bisimulation on finite relational structures admits polynomial-time canonisation, yielding linearly ordered representatives of each guarded-bisimulation class.The resulting invariant and canonisation are uniformly interpretable in IFP and LFP over powers of the input structures.Source: §6 · pp. 31–32
- Guarded-bisimulation-invariant polynomial time is captured by polynomial-time algorithms after canonisation, or equivalently by LFP or IFP on the ordered canonisations.Canonisation acts as preprocessing that enforces the required invariance.Source: §6 · pp. 31–32
- The ordered guarded-bisimulation invariant is a polynomial-time computable complete invariant, uniformly interpretable in IFP and LFP.It is obtained by ordering the quotient of the guarded-bisimulation game graph.Source: §6 · pp. 32–33
- The canonisation is constructed by applying an ordered Rosati cover to the ordered invariant and ordering the cover's terms.The paper states that this ordered representative is polynomial-time computable.Source: §6 · pp. 33–34