Antoine Amarilli Ltci

Michael Benedikt

Pierre Bourhis

Michael Vanden Boom

Query Answering with Transitive and Linear-Ordered Data

We consider entailment problems involving powerful constraint languages such as guarded existential rules, in which additional semantic restrictions are put on a set of distinguished relations. We consider restricting a relation to be transitive, restricting a relation to be the transitive closure of another relation, and restricting a relation to be a linear order. We give some natural generalizations of guardedness that allow inference to be decidable in each case, and isolate the complexity of the corresponding decision problems. Finally we show that slight changes in our conditions lead to undecidability.

. However, our results can be adapted to the case of reflexive and transitive predicates (and reflexive transitive closure).

Introduction

The query answering problem (or certain answer problem), abbreviated here as QA, is a fundamental reasoning problem in both knowledge representation and databases. It asks whether a query (e.g. given by an existentially-quantified conjunction of atoms) is entailed by a set of constraints and a set of facts. A common class of constraints used for QA are the existential rules, also known as tuple generating dependencies (TGDs). Although query answering is known to be undecidable for general TGDs, there are a number of subclasses that admit decidable QA, such as those based on guardedness. For instance, guarded TGDs require all variables in the body of the dependency to appear in a single body atom (the guard). Frontier-guarded TGDs (FGTGDs) relax this condition and require only that some guard atom contains the variables that occur in both head and body [START_REF] Baget | [END_REF]. This includes standard SQL referential constraints as well as important constraint classes (e.g. role inclusions) arising in knowledge representation. Guarded existential rules can be generalized to guarded logics that allow disjunction and negation and still enjoy decidable QA, e.g. the guarded fragment of first-order logic (GF) [START_REF] Andréka | [END_REF]] and the Guarded Negation Fragment (GNF) [Bárány et al., 2011].

A key challenge is to extend these results to capture additional semantics of the relations. For example, the property that a binary relation is transitive cannot be expressed directly in guarded logics, and neither can the property that one relation is the transitive closure of another. Going beyond transitivity, one cannot express that a binary relation is a linear order. Since ordered data is common in applications, this means that a key part of data semantics is being lost.

There has been extensive work on decidability results for guarded logics thus extended with semantic restrictions. We first review known results for the satisfiability problem. [START_REF] Ganzinger | [END_REF] showed that satisfiability is not decidable for GF when two relations are restricted to be transitive, even on arity-two signatures (i.e. with only unary and binary relations). For linear orders, [START_REF] Kieronski | Decidability issues for two-variable logics with several linear orders[END_REF] showed GF is undecidable when three relations are restricted to be (non-strict) linear orders, even with only two variables (so on arity-two signatures). Otto [2001] showed satisfiability is decidable for two-variable logic with one relation restricted to be a linear order. For transitive relations, one way to regain decidability for GF satisfiability was shown by [START_REF] Szwast | Wiesław Szwast and Lidia Tendera. The guarded fragment with transitive guards[END_REF]: allow transitive relations only in guards. We now turn to the QA problem. Gottlob et al. [2013] showed that query answering for GF with transitive relations only in guards is undecidable, even on arity-two signatures. [START_REF] Baget | [END_REF] studied QA with respect to a collection of linear TGDs (those with only a single atom in the body and the head). They showed that the query answering problem is decidable with such TGDs and transitive relations, if the signature is binary or if other additional restrictions are obeyed.

The case of TGDs mentioning relations with a restricted interpretation has been studied in the database community mainly in the setting of acyclic schemas, such as those that map source data to target data. Transitivity restrictions have not been studied, but there has been work on inequalities [Abiteboul and Duschka, 1998] and TGDs with arithmetic [START_REF] Afrati | [END_REF]. Due to the acyclicity assumptions, QA is still decidable, and has data complexity in CoNP. The fact that the data complexity can be CoNP-hard is shown in [Abiteboul and Duschka, 1998], while polynomial cases have been isolated in [Abiteboul and Duschka, 1998] (in the presence of inequalities) and [START_REF] Afrati | [END_REF] (in the presence of arithmetic).

Transitivity has also been studied in description logics, where the signature contains unary relations (concepts) and binary relations (roles). In this arity-two context, QA is decidable for many description logics featuring expressive operators as well as transitivity, such as ZIQ, ZOQ, ZOI [Cal-vanese et al., 2009], Horn-SROIQ [START_REF] Ortiz | [END_REF], or regular-EL ++ [START_REF] Krötzsch | Conjunctive queries for EL with role composition[END_REF], but they often restrict the interaction between transitivity and some features such as role inclusions and Boolean role combinations. QA becomes undecidable for more expressive description logics with transitivity such as ALCOIF ⇤ [START_REF] Ortiz | Query answering is undecidable in DLs with regular expressions, inverses, nominals, and counting[END_REF] and ZOIQ [START_REF] Ortiz De La Fuente | Maria Magdalena Ortiz de la Fuente. Query answering in expressive description logics[END_REF], and the problem is open for SROIQ and SHOIQ [START_REF] Ortiz | Magdalena Ortiz and Mantas Šimkus. Reasoning and query answering in description logics[END_REF]. The main contribution of this work is to introduce a broad class of constraints over arbitrary-arity vocabularies where query answering is decidable when additional semantics are imposed on some distinguished relations. We show that transitivity restrictions can be handled in guarded and frontierguarded constraints, as long as these distinguished relations are not used as guards -we call this new kind of restriction base-guardedness (and similarly, we extend frontier-guarded to "base-frontier-guarded" and so forth). The base-guarded restriction is orthogonal to the prior decidable cases such as transitive guards [START_REF] Szwast | Wiesław Szwast and Lidia Tendera. The guarded fragment with transitive guards[END_REF] or linear rules [START_REF] Baget | [END_REF].

On the one hand, we show that the condition allows us to define very expressive and flexible decidable logics, capable of expressing not only guarded existential rules, but guarded rules with negation and disjunction in the head. They can express not only integrity constraints but also conjunctive queries and their negations. On the other hand, a by-product of our results is new query answering schemes for some previously-studied classes of guarded existential rules with extra semantic restrictions. For example, our base-frontierguarded constraints encompass all frontier-one TGDs (where at most one variable is shared between the body and head) [Baget et al., 2009]. Hence, our results imply that QA is decidable with transitive closure and frontier-one constraints, which answers a question of [START_REF] Baget | [END_REF]. Our results even extend to frontier-one TGDs with distinguished relations that are required to be the transitive closure of other relations.

Our results are shown by arguing that it is enough to consider entailment over "tree-like" sets of facts. By representing the set of witness representations as a tree automaton, we derive upper bounds for the combined complexity of the problem. The sufficiency of tree-like examples also enable a refined analysis of data complexity (when the query and constraints are fixed). Further, we use a set of coding techniques to show matching lower bounds within our fragment. We also show that loosening our conditions leads to undecidability.

Finally, we solve the QA problem when the distinguished relations are linear orders. We show that it is undecidable even assuming base-guardedness, so we introduce a stronger condition called base-coveredness: not only are distinguished relations never used as guards, they are always covered by a non-distinguished atom. Our decidability technique works by "compiling away" linear order restrictions, obtaining an entailment problem without any special restrictions. The correctness proof for our reduction to classical QA again relies on the ability to restrict reasoning to sets of facts with treelike representations. To our knowledge, these are the first decidability results for the QA problem with linear orders. Again, we give tight complexity bounds, and show that weakening the base-coveredness condition leads to undecidability.

Preliminaries

We work on a relational signature where each relation R 2 has an associated arity (written arity(R)); we write arity( ) • • = max R2 arity(R). A fact R(ã) (or R-fact) consists of a relation R 2 and domain elements ã, with |ã| = arity(R). We denote a (finite or infinite) set of facts over by F. We write elems(F) for the set of elements mentioned in the facts in F.

We consider constraints and queries given in fragments of first-order logic (FO). For simplicity, we disallow constants in constraints and queries, although our results extend with them. Given a set of facts F and a sentence ' in FO, we talk of F satisfying ' in the usual way. The size of ', written |'|, is defined to be the number of symbols in '.

The queries that we will use are conjunctive queries (CQ), namely, existentially quantified conjunction of atoms, which we restrict for simplicity to be Boolean. We also allow unions of conjunctive queries (UCQs), namely, disjunctions of CQs.

Problems considered. Given a finite set of facts F 0 , constraints ⌃ and query Q (given as FO sentences), we say that F 0 and ⌃ entail Q if for every (possibly infinite) F ◆ F 0 satisfying ⌃, F satisfies Q. This amounts to asking whether F 0 ^⌃ ^¬Q is satisfiable (by a possibly infinite set of facts).

We write QA(F 0 , ⌃, Q) for this decision problem, called the query answering problem.

In this paper, we study the QA problem when imposing semantic constraints on some distinguished relations. We thus split the signature as • • = B t D , where B is the base signature (its relations are the base relations), and D is the distinguished signature. All distinguished relations are required to be binary, and they will be assigned special semantics. We study three kinds of special semantics.

We say F 0 , ⌃ entails Q over transitive relations, and write QAtr(F 0 , ⌃, Q) for the corresponding problem, if F 0 ^⌃ ¬Q is satisfied by some set of facts F where each distinguished relation R + i in D is required to be transitive 1 in F. We say F 0 , ⌃ entails Q over transitive closure, and write QAtc(F 0 , ⌃, Q) for this problem, if the same holds on some F where each relation R + i of D is interpreted as the transitive closure of a corresponding binary base relation R i 2 B . We say F 0 , ⌃ entails Q over linear orders, and write QAlin(F 0 , ⌃, Q), if the same holds on some F where each relation < i 2 D is required to be a strict linear order on the elements of F.

We now define the constraint languages (which are all fragments of FO) for which we study these QA problems.

Dependencies. The first constraint languages we study are restricted classes of tuple-generating dependencies (TGDs). A TGD is a first-order sentence ⌧ of the form 8x ( We will be interested in TGDs that are guarded in various ways. A guard for x is an atom from using every variable in x. We will be particularly interested in base-guards, which are guards coming from the base relations B .

A frontier-guarded TGD (FGTGD) is a TGD whose body contains a guard for the frontier variables -variables that occur in both head and body. It is a base frontier-guarded TGD (BaseFGTGD) if there is a base atom including all the frontier variables. We allow equality atoms x = x to be guards, so BaseFGTGD subsumes frontier-one TGDs, which have one frontier variable. Frontier-guarded and frontier-one TGDs have been shown to have an attractive combination of expressivity and computational properties [START_REF] Baget | [END_REF].

We also introduce the more restricted class of basecovered frontier-guarded TGDs (BaseCovFGTGD): they are the BaseFGTGDs where, for every D -atom in the body, there is a base atom in the body containing its variables (a base guard for the atom). Note that each D -atom may have a different base guard.

An important special case of frontier-guarded TGDs for applications are inclusion dependencies (ID). An ID is a FGTGD where the body and head contain a single atom, and no variable occurs twice in the same atom. A base inclusion dependency BaseID is an ID where the body atom is in B , so the body atom serves as the base-guard for the frontier variables, while the constraint is trivially base-covered.

Guarded logics. Moving beyond TGDs, the second kind of constraint that we study are guarded logics.

The guarded negation fragment (GNF) is the fragment of FO which contains all atoms, and is closed under conjunction, disjunction, existential quantification, and the following form of negation: for any GNF formula '(x) and atom A(x, ỹ) with free variables exactly as indicated, the formula A(x, ỹ)¬ '(x) is in GNF. That is, existential quantification may be unguarded, but the free variables in any negated subformula must be guarded; universal quantification must be expressed with existential quantification and negation. GNF can express all FGTGDs, as well as non-TGD constraints and UCQs. For instance, as it allows disjunction, GNF can express disjunctive inclusion dependencies, DIDs, which generalize IDs: their body is a single atom with no repeated variables, and their head is a disjunction of atoms with no repeated variables.

We introduce the base-guarded negation fragment BaseGNF over : it is defined like GNF, but requires base guards instead of guards. The base-covered guarded negation fragment BaseCovGNF over consists of BaseGNF formulas such that every D -atom A that appears negatively (i.e., under the scope of an odd number of negations) appears conjoined with a base guard -i.e., a B -atom containing all variables of A. This technical condition is designed to generalize BaseCovFGTGDs. Indeed, a BaseCovFGTGD of the form 8x(

V i ! 9ỹ V ⇢ i ) can be written in BaseCovGNF as ¬9x( V i ^¬9ỹ V ⇢ i ).
We call a CQ Q base-covered if each D -atom in Q has a B -atom of Q containing its variables. This is the same as saying that ¬Q is in BaseCovGNF. A UCQ is base-covered if each disjunct is.

Examples. We conclude the preliminaries by giving a few examples. Consider a signature with a binary base relation B, a ternary base relation C, and a distinguished relation

R + . • 8xyz (R + (x, y) ^R+ (y, z)) ! R + (x, z) is a TGD,
but is not a FGTGD since the frontier variables x, z are not guarded. It cannot even be expressed in GNF.

• 8xy R + (x, y) ! B(x, y) is an ID, hence a FGTGD.
It is not a BaseID or even in BaseGNF, since the frontier variables are not base-guarded.

• 8xyz (B(z, x) ^R+ (x, y) ^R+ (y, z)) ! R + (x, z) is a BaseFGTGD.
It is not a BaseCovFGTGD since there are no base atoms in the body to cover x, y and y, z.

• 9wxyz R + (w, x) ^R+ (x, y) ^R+ (y, z) ^R+ (z, w) Ĉ(w, x, y) ^C(y, z, w) is a base-covered CQ. • 9xy B(x, y) ^¬(R + (x, y) ^R+ (y, x)) ^(R + (x, y) _ R + (y, x)
) cannot be rewritten as a TGD. But it is in BaseCovGNF.

Our main results are summarized in Table a, and the languages that we study are illustrated in Figure b. In particular, QAtr and QAtc are decidable for BaseGNF. This includes base-frontier-guarded rules, which allow one to use a transitive relation such as "part-of" (or even its transitive closure) whenever only one variable is to be exported to the head. This latter condition holds in the translations of many classical description logics. Our results also imply that QAlin is decidable for BaseCovGNF, which allows constraints that arise from data integration and data exchange over attributes with linear orders -e.g. views defined by selecting rows of a table where some inequality involving the attributes is satisfied.

We first consider QAtc, where B includes binary relations R 1 , . . . , R n , and D consists of binary relations R + 1 , . . . , R + n such that R + i is the transitive closure of R i . Theorem 1. We can decide QAtc(F 0 , ⌃, Q) in 2EXPTIME, where F 0 ranges over finite sets of facts, ⌃ over BaseGNF constraints, and Q over UCQs. In particular, this holds when ⌃ consists of BaseFGTGDs.

In order to prove Theorem 1, we give a decision procedure to determine whether F 0 ^⌃ ^¬Q is satisfiable, when

R + i is interpreted as the transitive closure of R i . When ⌃ 2 BaseGNF and Q is a Boolean UCQ, then ⌃ ^¬Q is
in BaseGNF. So it suffices to show that BaseGNF satisfiability is decidable, when properly interpreting R + i . As mentioned in the introduction, our proofs rely heavily on the fact that in query answering problems for these constraint languages, one can restrict to sets of facts that have a "tree-like" structure. We now make this notion precise. A tree decomposition of F consists of a tree (T, Child) and a labelling function associating each node of the tree T to a set of facts of F, called the bag of that node, that satisfies the following conditions: (i) each fact of F must be in the image of ; (ii) for each element e 2 elems(F), the set of nodes whose bag uses e is a connected subset of T . It is F 0 -rooted if the root node is associated with F 0 . It has width k 1 if each bag other than the root mentions at most k elements.

For a number k, a sentence ' is said to have transitiveclosure friendly k-tree-like witnesses if: for every finite set of facts F 0 , if there is an F extending F 0 with additional Bfacts such that F satisfies ' when each R + is interpreted as the transitive closure of R, then there is such an F that has an F 0 -rooted (k 1)-width tree decomposition. We can show that BaseGNF sentences have this kind of k-tree-like witness for an easily computable k. The proof uses a standard technique, involving an unravelling based on "guarded negation bisimulation" [Bárány et al., 2011]: Proposition 1. Every sentence ' in BaseGNF has transitiveclosure friendly k-tree-like witnesses, where k  |'|.

Here k can be taken to be the "width" of ' [Bárány et al., 2011], which is roughly the maximum number of free variables in any subformula. Hence, it suffices to test satisfiability for BaseGNF restricted to sets of facts with tree decompositions of width |'| 1. It is well known that sets of facts of bounded tree-width can be encoded as trees over a finite alphabet that depends only on the signature and the tree-width. This makes the problem amenable to tree automata techniques, since we can design a tree automaton that runs on representations of these tree decompositions and checks whether some sentence holds in the corresponding set of facts. Theorem 2. Let ' be a sentence in BaseGNF, and let F 0 be a finite set of facts. We can construct in 2EXPTIME a 2-way alternating parity tree automaton A ',F0 such that

F 0 ^' is satisfiable iff L(A ',F0 ) 6 = ; when each R + i 2 D is interpreted as the transitive closure of R i 2 B . The number of states of A ',F0 is exponential in |'| • |F 0 | and the number of priorities is linear in |'|.
The construction can be viewed as an extension of [START_REF] Calvanese | Decidable containment of recursive queries[END_REF], and incorporates ideas from automata for guarded logics (see, e.g., [START_REF] Grädel | Guarded fixed point logic[END_REF]). Because 2-way tree automata emptiness is decidable in time exponential in the number of states and priorities [Vardi, 1998], this yields the 2EXPTIME bound for Theorem 1.

Consequences for QAtr. We can derive results for QAtr by observing that the QAtc problem subsumes it: to enforce that R + 2 D is transitive, simply interpret it as the transitive closure of a relation R that is never otherwise used. Hence: Corollary 1. We can decide QAtr(F 0 , ⌃, Q) in 2EXPTIME, where F 0 ranges over finite sets of facts, ⌃ over BaseGNF constraints (in particular, BaseFGTGD), and Q over UCQs.

In particular, this result holds for frontier-one TGDs (those with a single frontier variable), as a single variable is always base-guarded. This answers a question of [START_REF] Baget | [END_REF].

Data complexity. Our results in Theorem 1 and Corollary 1 show upper bounds on the combined complexity of the QAtr and QAtc problems. We now turn to the complexity when the query and constraints are fixed but the initial set of facts varies -the data complexity.

We first show a CoNP data complexity upper bound for QAtc for BaseGNF constraints. The algorithm uses the fact that a counterexample to QAtc can be taken to have a F 0 rooted tree decomposition, for some F 0 that does not add new elements to F 0 , only new facts. While such a decomposition could be large, it suffices to guess F 0 and annotations describing, for each |'|-tuple c in F 0 , sufficiently many formulas holding in the subtree that interfaces with c. The technique generalizes an analogous result in [Bárány et al., 2012]. Theorem 3. For any fixed BaseGNF constraints ⌃ and UCQ Q, given a finite set of facts F 0 , we can decide QAtc(F 0 , ⌃, Q) in CoNP data complexity.

For FGTGDs, the data complexity of QA is in PTIME [START_REF] Baget | [END_REF]. We can show that the same holds, but only for BaseCovFGTGDs, and for QAtr rather than QAtc: Theorem 4. For any fixed BaseCovFGTGD constraints ⌃ and base-covered UCQ Q, given a finite set of facts F 0 , we can decide QAtr(F 0 , ⌃, Q) in PTIME data complexity.

The proof uses a reduction to the standard QA problem for FGTGDs, and then applies the PTIME result of [START_REF] Baget | [END_REF]. The reduction again makes use of tree-likeness to show that we can replace the requirement that the R + i are transitive by the weaker requirement of transitivity within small sets (intuitively, within bags of a decomposition). We will also use this idea for linear orders (see Proposition 3).

Restricting to QAtr is in fact essential to make data complexity tractable, as hardness holds otherwise.

Hardness. We now show complexity lower bounds. We already know that all our variants of QA are 2EXPTIME-hard in combined complexity, and CoNP-hard in data complexity, when GNF constraints are allowed: this follows from existing bounds on GNF reasoning [Bárány et al., 2012] even without distinguished predicates. However, in the case of the QAtc problem, we can show the same result for the much weaker language of BaseIDs.

We do this via a reduction from QA with disjunctive inclusion dependencies, which is known to be 2EXPTIME-hard in combined complexity [Bourhis et al., 2013, Theorem 2] and CoNP-hard in data complexity [START_REF] Calvanese | Data complexity of query answering in description logics[END_REF][START_REF] Bourhis | [END_REF], even without distinguished relations. We use the transitive closure to emulate disjunction (as was already suggested in the description logic context [START_REF] Horrocks | Ian Horrocks and Ulrike Sattler. A description logic with transitive and inverse roles and role hierarchies[END_REF]) by creating an R + i -fact and limiting the length of a witness R i -path (this limit is imposed by Q 0

). The choice of the length of the witness path among two possibilities is used to mimic the disjunction. We thus show: Theorem 5. For any finite set of facts F 0 , DIDs ⌃, and UCQ Q on a signature , we can compute in PTIME a set of facts F 0 0 , BaseIDs ⌃ 0 , and a base-covered CQ Q 0 on a signature 0 (with a single distinguished relation), such that QA(F 0 , ⌃, Q) iff QAtc(F 0 0 , ⌃ 0 , Q 0 ). This implies the following, contrasting with Theorem 4: Corollary 2. The QAtc problem with BaseIDs and basecovered CQs is CoNP-hard in data complexity and 2EXPTIME-hard in combined complexity.

In fact, the data complexity lower bound for QAtc even holds in the absence of constraints: Proposition 2. There is a base-covered CQ Q such that the data complexity of QAtc(F 0 , ;, Q) is CoNP-hard.

We prove this by reducing the problem of 3-coloring a directed graph, known to be NP-hard, to the complement of QAtc. It is well-known how to do this using TGDs that have disjunction in the head. As in the proof of Theorem 5, we simulate this disjunction by using a choice of the length of paths that realize transitive closure facts asserted in F 0 .

In all of these hardness results, we first prove them for UCQs, and then show how the use of disjunction can be eliminated, using a prior "trick" (see, e.g., [START_REF] Gottlob | On the complexity of single-rule datalog queries[END_REF]) to code the intermediate truth values of disjunctions within a CQ.

Decidability results for linear orders

We now move to QAlin, the setting where the distinguished relations < i of D are linear (total) strict orders, i.e., they are transitive, irreflexive, and total. We consider constraints and queries that are base-covered. We prove the following result. Theorem 6. We can decide QAlin(F 0 , ⌃, Q) in 2EXPTIME, where F 0 ranges over finite sets of facts, ⌃ over BaseCovGNF, and Q over base-covered UCQs. In particular, this holds when ⌃ consists of BaseCovFGTGDs.

Our technique here is to reduce this to traditional QA where no additional restrictions (like being transitive or a linear order) are imposed. Starting with BaseCovGNF constraints, we reduce to a traditional QA problem with GNF constraints, and hence prove decidability in 2EXPTIME using [Bárány et al., 2012]. However, the reduction is quite simple, and hence could be applicable to other constraint classes.

The idea behind the reduction is to include additional constraints that enforce the linear order conditions. However, we cannot express transitivity or totality in GNF. Hence, we will only add a weakening of these properties that is expressible in GNF, and then argue that this is sufficient for our purposes.

The reduction is described in the following proposition. Proposition 3. For any finite set of facts F 0 , constraints ⌃ 2 BaseCovGNF, and base-covered UCQ Q, we can compute F 0 0 and

⌃ 0 2 BaseGNF in PTIME such that QAlin(F 0 , ⌃, Q) iff QA(F 0 0 , ⌃ 0 , Q).
In particular, F 0 0 is F 0 together with facts G(a, b) for every pair a, b 2 elems(F 0 ), where G is some fresh binary base relation. We define ⌃ 0 as ⌃ together with the k-guardedly linear axioms for each distinguished relation <, where k is max(|⌃ ^¬Q|, arity( [ {G})); namely:

• guardedly total:

8xy((guarded B [{G} (x, y)^x 6 = y) ! x < y _y < x) • irreflexive: ¬9x(x < x) • k-guardedly transitive: for 1  l  k 1: ¬9xy( l (x, y) ^guarded B [{G} (x, y) ^¬(x < y)) and, for 1  l  k: ¬9x( l (x, x) ^x = x ^¬(x < x))
where:

• guarded B [{G} (x, y) is the formula expressing that x, y is base-guarded (an existentially-quantified disjunction over all possible base-guards containing x and y);

• 1 (x, y) is just x < y; and • l (x, y) for l 2 is: 9x 2 . . . x l (x < x 2 ^• • • ^xl < y).
Unlike the property of being a linear order, the k-guardedly linear axioms can be expressed in BaseGNF.

We now sketch the argument for the correctness of the reduction. The easy direction is where we assume QA(F 0 0 , ⌃ 0 , Q) holds, so any F 0 ◆ F 0 0 satisfying ⌃ 0 must satisfy Q. Now consider F ◆ F 0 that satisfies ⌃ and where all < in D are strict linear orders. We must show that F satisfies Q. First, observe that F satisfies ⌃ 0 since the k-guardedly linear axioms for < are clearly satisfied for all k when < is a strict linear order. Now consider the extension of F to F 0 with facts G(a, b) for all a, b 2 elems(F 0 ). This must still satisfy ⌃ 0 : adding these facts means there are additional k-guardedly linear requirements on the elements from F 0 , but these requirements already hold since < is a strict linear order. Hence, by our initial assumption, F 0 must satisfy Q. Since Q does not mention G, the restriction of F 0 back to F still satisfies Q as well. Therefore, QAlin(F 0 , ⌃, Q) holds.

For the harder direction, suppose for the sake of contradiction that QA(F 0 0 , ⌃ 0 , Q) does not hold, but QAlin(F 0 , ⌃, Q) does. Then there is some F 0 ◆ F 0 0 such that F 0 satisfies ⌃ 0 ^¬Q. We will again rely on the ability to restrict to treelike F 0

, but with a slightly different notion of tree-likeness. We say a set E of elements from elems(F) are baseguarded in F if there is some B -fact or G-fact in F that mentions all of the elements in E. A base-guarded-interface tree decomposition (T, Child, ) for F is a tree decomposition satisfying the following additional property: for all nodes n 1 that are not the root of T , if n 2 is a child of n 1 and E is the set of elements mentioned in both n 1 and n 2 , then E is base-guarded in F. A sentence ' has base-guarded-interface k-tree-like witnesses if for any finite set of facts F 0 , if there is some F ◆ F 0 satisfying ' then there is such an F with an F 0 -rooted (k 1)-width base-guarded-interface tree decomposition.

Although the transformation from ⌃ to ⌃ 0 makes the formula larger, it does not increase the "width" that controls the bag size of tree-like witnesses. Hence, we can show: Lemma 1. The sentence ⌃ 0 ^¬Q has base-guarded-interface k-tree-like witnesses for k = max(|⌃^¬Q|, arity( [{G})).

Using this lemma, we can assume that we have some F 0 ◆ F 0 0 which has a (k 1)-width base-guarded-interface tree decomposition and witnesses ⌃ 0 ^¬Q. If every < in D is a strict linear order in F 0

, then restricting F 0 to the set of -facts yields some F that would satisfy ⌃ ^¬Q, a contradiction. Hence, there are some distinguished relations < that are not strict linear orders in F 0

. We can show that such an F 0 can actually be extended to some F 00 that still satisfies ⌃ 0 ^¬Q but where all < in D are strict linear orders, which we already argued is impossible.

The crucial part of the argument is thus about extending k-guardedly linear counterexamples to genuine linear orders: Lemma 2. If there is F 0 ◆ F 0 0 that satisfies ⌃ 0 ^¬Q and has a F 0 0 -rooted base-guarded-interface (k 1)-width tree decomposition, then there is F 00 ◆ F 0 that satisfies ⌃ 0 ^¬Q where each distinguished relation is a strict linear order.

The proof of Lemma 2 proceeds by showing that sets of facts that have (k 1)-width base-guarded-interface tree decompositions and satisfy k-guardedly linear axioms must already be cycle-free with respect to <. Hence, by taking the transitive closure of < in F, we get a new set of facts where every < is a strict partial order. Any strict partial order can be further extended to a strict linear order using known techniques, so we can obtain F 00 ◆ F 0 where < is a strict partial order. This F 00 may have more <-facts than F 0 , but the k-guardedly linear axioms ensure that these new <-facts are only about pairs of elements that are not base-guarded.

It remains to show that F 00 satisfies ⌃ 0 ^¬Q. It is clear that F 00 still satisfies the k-guardedly linear axioms, but it could no longer satisfy ⌃ ^¬Q. However, this is where the base-covered assumption on ⌃ ^¬Q is used: it can be shown that satisfiability of ⌃ ^¬Q in BaseCovGNF is not affected by adding new <-facts about pairs of elements that are not base-guarded.

Data complexity. Again, the result of Theorem 6 is a combined complexity upper bound. However, as it works by reducing to traditional QA in PTIME, data complexity upper bounds follow from [Bárány et al., 2012]. Corollary 3. For any BaseCovGNF constraints ⌃ and basecovered UCQ Q, given a finite set of facts F 0 , we can decide QAlin(F 0 , ⌃, Q) in CoNP data complexity. This is similar to the way data complexity bounds were shown for QAtr (in Theorem 4). However, unlike for the QAtr problem, the constraint rewriting in this section introduces disjunction, so rewriting a QAlin problem for BaseCovFGTGDs does not produce a classical query answering problem for FGTGDs. Thus the rewriting does not imply a PTIME data complexity upper bound for BaseCovFGTGD. Indeed, we will see in Proposition 4 that this is CoNP-hard.

Hardness. QAlin for BaseCovGNF constraints is again immediately CoNP-hard in data complexity, and 2EXPTIMEhard in combined complexity, from the corresponding bounds on GNF [Bárány et al., 2012]. However, we can show that hardness holds for the much weaker constraint language BaseID, by a reduction from DID reasoning, as in Section 3.

Theorem 7. For any finite set of facts F 0 , DIDs ⌃, and UCQ Q on a signature , we can compute in PTIME a set of facts F 0 0 , BaseIDs ⌃ 0 , and CQ Q 0 on a signature 0 (with a single distinguished relation), such that QA(F 0 , ⌃, Q) iff QAlin(F 0 0 , ⌃ 0 , Q 0 ). The reduction allows us to transfer hardness results for DID from [START_REF] Calvanese | Data complexity of query answering in description logics[END_REF][START_REF] Bourhis | [END_REF], exactly as was done in Theorem 5, to conclude: Corollary 4. The QAlin problem with BaseID and basecovered CQs is CoNP-hard in data complexity and 2EXPTIME-hard in combined complexity.

Again, as in the previous section, the data complexity lower bound even holds in the absence of constraints: Proposition 4. There is a base-covered CQ Q such that the data complexity of QAlin(F, ;, Q) is CoNP-hard.

Undecidability results for transitivity

We have shown in Section 3 that query answering is decidable with transitive relations (even with transitive closure), BaseFGTGDs, and UCQs (Theorem 1). Removing our base-guarded condition leads to undecidability of QAtc, even when constraints are inclusion dependencies: Theorem 8. There is a signature = B t D with a single distinguished predicate S + in D , a set ⌃ of IDs on , and a CQ Q on B , such that the following problem is undecidable: given a finite set of facts F 0 , decide QAtc(F 0 , ⌃, Q).

The proof is by reduction from a tiling problem. The constraints use a transitive successor relation to define a grid of integer pairs. It then uses transitive closure to emulate disjunction, as in Theorem 5, and relies on Q to test for forbidden adjacent tile patterns.

An analogous result can be shown for QAtr, using (nonbase-guarded) disjunctive inclusion dependencies: Theorem 9. There is an arity-two signature = B t D with a single distinguished predicate S + in D , a set ⌃ of DIDs on , a CQ Q on B , such that the following problem is undecidable: given a finite set of facts F 0 , decide QAtr(F 0 , ⌃, Q).

These results complement the undecidability results of [Gottlob et al., 2013, Theorem 2], which showed that, on arity-two signatures, QAtr is undecidable with guarded TGDs and atomic CQs, even when transitive relations occur only in guards. Our results also contrast with the decidability results of [START_REF] Baget | [END_REF] which apply to QAtr: our Theorem 8 shows that their results cannot extend to QAtc.

Section 4 has shown that QAlin is decidable for base-covered CQs and BaseCovGNF constraints. Dropping the basecovered requirement on the query leads to undecidability: Theorem 10. There is a signature = B t D where D is a single strict linear order relation, a CQ Q on , and a set ⌃ of inclusion dependencies on B (i.e., not mentioning the linear order, so in particular base-covered), such that the following problem is undecidable: given a finite set of facts F 0 , decide QAlin(F 0 , ⌃, Q).

This result is close to [Gutiérrez-Basulto et al., 2013, Theorem 3], which deals not with a linear order, but inequalities in queries, which we can express with a linear order. However, this requires a UCQ. As in our prior hardness and undecidability results, we can adapt the technique to use a CQ.

By letting ⌃ 0 • • = ⌃ ^¬Q where ⌃ and Q are as in the previous theorem, we obtain base-guarded constraints for which QAlin is undecidable. In fact, ⌃ 0 can be expressed as a set of BaseFGTGDs. This implies that the base-covered requirement is necessary for the constraint language: Corollary 5. There is a signature = B t D where D is a single strict linear order relation, and a set ⌃ 0 of BaseFGTGD constraints, such that, letting > be the tautological query, the following problem is undecidable: given a finite set of facts F 0 , decide QAlin(F 0 , ⌃ 0 , >).

Conclusion

We have given a detailed picture of the impact of transitivity, transitive closure, and linear order restrictions on query answering problems for a broad class of guarded constraints.

We have shown that transitive relations and transitive closure restrictions can be handled in guarded constraints as long as they are not used in guards. For linear orders, the same is true if order atoms are covered by base atoms. This implies the analogous results for frontier-guarded TGDs, in particular frontier-one. But in the linear order case we show that PTIME data complexity cannot always be preserved.

We leave open the question of entailment over finite sets of facts. There are few techniques for deciding entailment over finite sets of facts for logics where it does not coincide with general entailment (and for the constraints considered here it does not coincide). An exception is [START_REF] Bárány | [END_REF]], but it is not clear if the techniques there can be extended to our constraint languages.

The proofs for the results stated in the main paper are provided in this appendix.

A Normal form

The proofs make use of the fact that the fragments of GNF that we consider can be converted into a normal form that is related to the GN normal form introduced in the original paper on GNF [Bárány et al., 2011]. The idea is that GNF formulas can be seen as being built up from atoms using guarded negation, disjunction, and CQs. We introduce this normal form here, and discuss some related notions we will use in the proofs.

First, the guardedness predicate guarded(x) asserts that x is guarded by some -atom; it can be seen as an abbreviation for the disjunction of existentially quantified relational atoms from involving all of the variables from x. We write guarded B (x) for the corresponding guardedness predicate restricted to B .

The normal form for BaseGNF over starts with B -atoms and builds up via the following rules:

• If ' 1 (x) and ' 2 (x) are in normal form BaseGNF, then

' 1 (x) _ ' 2 (x) are in normal form BaseGNF. • If '(x) is in normal form BaseGNF and A(x) is a B - atom or the B -guardedness predicate, then A(x) ¬'(x)
is in normal form BaseGNF. Likewise, the normal form for BaseCovGNF over consists of normal form BaseGNF formulas such that for every CQ-shaped subformula that appears negatively (in the scope of an odd number of negations), and for every conjunct in , there must be some B -atom or B -guardedness predicate in that contains the free variables of .

Width and CQ-rank. For ' in normal form BaseGNF, we define the width of ' to be the maximum number of free variables in any subformula of '. The CQ rank of ' is the maximum number of conjuncts in any CQ-shaped subformula 9x( V i ) where x is non-empty. These will be important parameters in later proofs.

We write BaseGNF k to denote normal form BaseGNF formulas of width k, and similarly for BaseCovGNF k .

Conversion into normal form. Observe that formulas in BaseFGTGD or BaseCovFGTGD are of the form 8x(

V i ! 9ỹ V ⇢ i )
already and thus can be naturally written in normal form BaseGNF or BaseCovGNF as ¬9x(

V i ¬9ỹ V ⇢ i )
, with no blow-up in the size or width. In general, BaseGNF formulas can be converted into normal form, but with an exponential blow-up in size.

Proposition 5. Let ' be a formula in BaseGNF. We can construct an equivalent ' 0 in normal form in EXPTIME such that

• |' 0 | is at most exponential in |'|;
• the width of ' 0 is at most |'|;

• the CQ-rank of ' 0 is at most |'|;

• if ' is in BaseCovGNF, then ' 0 is in normal form BaseCovGNF.

Proof sketch. The conversion works by using the same rewrite rules as in [Bárány et al., 2011]:

9x(✓ _ ) ! (9x✓) _ (9x ) ✓ ^( _ ) ! (✓ ^ ) _ (✓ ^ ) 9x(✓) ^ ! 9x 0 (✓[x 0 /x] ^ ) where x 0 is fresh
The size, width, and CQ-rank bounds after performing this rewriting are straightforward to check.

The rewrite rules preserve the polarity of subformulas, which helps ensure that coveredness is preserved during this conversion. That is, for every ' in BaseGNF and for every finite set of facts F 0 , if there is any F extending F 0 with B -facts and satisfying ' when each relation R + is interpreted as the transitive closure of R, then there is some F like this that has a F 0 -rooted (k 1)-width tree decomposition.

If |'| < 3, then ' is necessarily a single 0-ary relation or its negation, in which case the result is trivial, with k = 1. Hence, in the rest of this section, we will assume that |'| 3 and k will be chosen such that 3  k  |'| (k will be an upper bound on the maximum number of free variables in any subformula of ').

The proof uses a standard technique, involving an unravelling related to a variant of guarded negation bisimulation [Bárány et al., 2011]. A related result and proof also appears in [Benedikt et al., 2016].

Bisimulation game. The GN k bisimulation game between sets of facts F and G is an infinite game played by two players, Spoiler and Duplicator. The game has two types of positions:

i) partial isomorphisms f : F X ! G Y or g : G Y ! F
X , where X ⇢ elems(F) and Y ⇢ elems(G) are both finite and are B -guarded;

ii) partial rigid homomorphisms f :

F X ! G Y or g : G Y ! F X ,
where X ⇢ elems(F) and Y ⇢ elems(G) are both finite and are of size at most k.

A partial rigid homomorphism is a partial homomorphism with respect to all -facts, such that the restriction to any Bguarded set of elements is a partial isomorphism.

From a type (i) position h, Spoiler must choose a finite subset X ⇢ elems(F) or a finite subset Y ⇢ elems(G), in either case of size at most k, upon which Duplicator must respond by a partial rigid homomorphism with domain X or Y accordingly, mapping it into the other set of facts in a manner consistent with h.

From a type (ii) position h : X ! Y (respectively, h : Y ! X), Spoiler must choose a finite subset X ⇢ elems(F) (respectively, Y ⇢ elems(G)) of size at most k, upon which Duplicator must respond by a partial rigid homomorphism with domain X (respectively, domain Y ), mapping it into the other set of facts in a manner consistent with h.

Notice that a type (i) position is a special kind of type (ii) position where Spoiler has the option to switch the domain to the other set of facts, rather than just continuing to play in the current domain.

Spoiler wins if he can force the play into a position from which Duplicator cannot respond, and Duplicator wins if she can continue to play indefinitely.

A winning strategy for Duplicator in the GN k bisimulation game implies agreement between F and G on certain BaseGNF formulas. Proposition 6. Let '(x) be a formula in BaseGNF, and let k 3 be greater than or equal to the maximum number of free variables in any subformula of '.

If Duplicator has a winning strategy in the GN k bisimulation game between F and G starting from a type (i) or (ii) position ã 7 ! b and F satisfies '(ã) when interpreting each

R + 2 D as the transitive closure of R 2 B , then G satis- fies '( b) when interpreting each R + 2 D as the transitive closure of R 2 B .
Proof. For this proof, when we talk about sets of facts satisfying a formula, we mean satisfaction when interpreting R + 2 D as the transitive closure of R 2 B . We will abuse terminology slightly and say that ' has width k if the maximum number of free variables in any subformula of ' is at most k (this is abusing the terminology since we are not assuming in this proof that ' is in normal form).

We proceed by induction on the number of D -atoms in ' and the size of '.

Suppose Duplicator has a winning strategy in the GN k bisimulation game between F and G.

If ' is a B -atom A(x), the result follows from the fact that the position ã 7 ! b is a partial homomorphism.

Suppose

' is a D -atom R + (x 1 , x 2 ), and ã = a 1 a 2 and b = b 1 b 2 . If F,ã satisfies R + (x 1 , x 2 )
, there is some n 2 N such that n > 0 and there is an R-path of length n between a 1 and a 2 in F. We can write a formula n (x 1 , x 2 ) in BaseGNF (without any D -atoms) that is satisfied exactly when there is an R-path of length n. Since we do not need to write this in normal form, we can express n in BaseGNF with width 3 (maximum of 3 free variables in any subformula). Since F,ã satisfies n and n does not have any D -atoms and k 3, we can apply the inductive hypothesis from the type (ii) position ã 7 ! b to ensure that G, b satisfies n , and hence G, b satisfies '.

If ' is a disjunction, the result follows easily from the inductive hypothesis.

Suppose ' is a base-guarded negation A(x) ^¬' 0 (x 0 ). By definition of BaseGNF, it must be the case that A 2 B and x0 is a sub-tuple of x. Since F,ã satisfies ', we know that F,ã satisfies A(x), and hence ã is B -guarded. This means that ã 7 ! b is actually a partial isomorphism, so we can view it as a position of type (i). This ensures that G, b also satisfies A(x). It remains to show that it satisfies ¬' 0 (x 0 ). Assume for the sake of contradiction that it satisfies ' 0 (x 0 ). Because ã 7 ! b is a type (i) position, we can consider the move in the game where Spoiler switches the domain to the other set of facts, and then restricts to the elements in the subtuple b0 of b corresponding to x0 in x. Let ã0 be the corresponding subtuple of ã. Duplicator must have a winning strategy from the type (i) position b0 7 ! ã0 , so the inductive hypothesis ensures that F,ã 0 satisfies ' 0 (x 0 ), a contradiction. Finally, suppose ' is an existentially quantified formula 9y(' 0 (x, y)). We are assuming that F,ã satisfies '. Hence, there is some c 2 elems(F) such that F,ã, c satisfies ' 0 . Because the width of ' is at most k, we know that the combined number of elements in ã and c is at most k. Hence, we can consider the move in the game where Spoiler selects the elements in ã and c. Duplicator must respond with b for ã, and some d for c. This is a valid move in the game, so Duplicator must still have a winning strategy from this position ãc 7 ! bd, and the inductive hypothesis implies that G, b, d satisfies ' 0 . Consequently, G, b satisfies '.

Unravelling. The tree-like witnesses can be obtained using an unravelling construction related to the GN k bisimulation game. This unravelling construction is adapted from [Benedikt et al., 2016].

Fix a set of facts F ◆ F 0 . Consider the set ⇧ of sequences of the form X 0 X 1 . . . X n , where X 0 = elems(F 0 ), and for all i 1, X i ✓ elems(F) with |X i |  k. We can arrange these sequences in a tree based on the prefix order. Each sequence ⇡ = X 0 X 1 . . . X n identifies a unique node in the tree; we say a is represented at node ⇡ if a 2 X n . For a 2 elems(F), we say ⇡ and ⇡ 0 are a-equivalent if a is represented at every node on the unique minimal path between ⇡ and ⇡ 0 in this tree. For a represented at ⇡, we write [⇡, a] for the a-equivalence class.

The GN k -unravelling of F is a set of facts F k over el- ements {[⇡, a] : ⇡ 2 ⇧ and a 2 elems(F)}. The fact R([⇡ 1 , a 1 ], . . . , [⇡ j , a j ]) 2 F k iff R(a 1 , . . . , a j ) 2 F and there is some ⇡ 2 ⇧ such that for all i, [⇡, a i ] = [⇡ i , a i ].
We can identify [✏, a] with the element a 2 elems(F 0 ), so there is a natural F 0 -rooted tree decomposition of width k 1 for F k induced by the tree of sequences from ⇧. Because this unravelling is related so closely to the GN k bisimulation game, it is straightforward to show that Duplicator has a winning strategy in the bisimulation game between F and its unravelling.

Proposition 7. Duplicator has a winning strategy in the GN k bisimulation game between F and F k .

Proof. Given a position f in the GN k -bisimulation game, we say the active set is the set of facts containing the elements in the domain of f . In other words, the active set is either F or F k , depending on which set Spoiler is currently playing in. The safe positions f in the GN k -bisimulation game between F and F k are defined as follows: if the active set is

F k , then f is safe if for all [⇡, a] 2 Dom(f ), f ([⇡, a]) = a; if the active set is F, then f is safe if there is some ⇡ such that f (a) = [⇡, a] for all a 2 Dom(f ).
We now argue that starting from a safe position f , Duplicator has a strategy to move to a new safe position f 0 . This is enough to conclude that Duplicator has a winning strategy in the GN k -bisimulation game between F and F k starting from any safe position.

First, assume that the active set is

F k . • If f is a type (ii) position, then Spoiler can select some new set X 0 of elements from the active set. Each el- ement in X 0 is of the form [⇡ 0 , a 0 ]. Duplicator must choose f 0 such that [⇡ 0 , a 0 ] is mapped to a 0
in F, in order to maintain safety. This new position f 0 is consistent with f on any elements in X 0 \ Dom(f ) since f is safe. This f 0 is still a partial homomorphism since any relation holding for a tuple of elements a 0 ] and[⇡ 0 , a 0 ] are not base-guarded in F k . Hence, any restriction f 00 of f 0 to a base-guarded set of elements is a bijection. Moreover, such an f 00 is a partial isomorphism: consider some a 1 , . . . , a n in the range of f 00 for which some relation S holds in F; since (f 00 ) 1 (a 1 ), . . . , (f 00 ) 1 (a n ) must be base-guarded, we know that there is some

[⇡ 1 , a 1 ], . . . , [⇡ n , a n ] from Dom(f 0 ) must hold for the tuple of elements a 1 , . . . , a n in F by definition of F k . Consider some el- ement [⇡ 0 , a 0 ] in Dom(f 0 ). It is possible that there is some [⇡, a 0 ] in Dom(f 0 ) with [⇡, a 0 ] 6 = [⇡ 0 , a 0 ]; how- ever, [⇡,
⇡ such that [⇡, a 1 ] = (f 00 ) 1 (a 1 ),. . . , [⇡, a n ] = (f 00 ) 1 (a n ), so by definition of F k
, S holds of (f 00 ) 1 (a 1 ), . . . , (f 00 ) 1 (a n ) as desired. Hence, f 0 is a safe partial rigid homomorphism. • If f is a type (i) position, then Spoiler can either choose elements in the active set and we can reason as we did for the type (ii) case, or Spoiler can select elements from the other set of facts. We first argue that if Spoiler changes the active set and chooses no new elements, then the game is still in a safe position. Since f is a type (i) position, we know that Dom(f ) is guarded by some base relation S, so there

is some ⇡ with f (a) = [⇡, a] for all a 2 Dom(f ) by construction of F k
. Hence, the new position f 0 = f 1 is still safe. If Spoiler switches active sets and chooses new elements, then we can view this as two separate moves: in the first move, Spoiler switches active sets from F k to F but chooses no new elements, and in the second move, Spoiler selects the desired new elements from F. Because switching active sets leads to a safe position (by the argument in the previous paragraph), it remains to define Duplicator's safe strategy when the active set is F, which we explain below. Now assume that the active set is F. Since f is safe, there is some ⇡ such that f (a) = [⇡, a] for all a 2 Dom(f ).

• If f is a type (ii) position, then Spoiler can select some new set X 0 of elements from the active set. We define the new position f 0 chosen by Duplicator to map each element

a 0 2 X 0 to [⇡ 0 , a 0 ] where ⇡ 0 = ⇡ • X 0
. By construction of the unravelling, ⇡ 0 2 ⇧ and the resulting partial mapping f 0 still satisfies the safety property with ⇡ 0 as witness. Note that f 0 is consistent with f for elements of X 0 that are also in Dom(f ), as we have

[⇡ • X 0 , a 0 ] = [⇡, a 0 ] for a 0 2 X 0 \ Dom(f ). Now consider some tuple ã = a 1 . . . a
n of elements from Dom(f 0 ) that are in some relation S. We know that

f 0 (a i ) = [⇡ 0 , a i ],
hence S must hold for f 0 (ã) in F k . Moreover, for any base-guarded set ã = {a 1 , . . . , a n } of distinct elements from Dom(f 0 ), f 0 (ã) must yield a set of distinct elements {f 0 (a 1 ), . . . , f 0 (a n )}, and these elements can only participate in some fact in F k if the underlying elements from ã participate in the same fact in F. Hence, f 0 is a safe partial rigid homomorphism. • If f is a type (i) position, then Spoiler can either choose elements in the active set and we can reason as we did for the type (ii) case, or Spoiler can select elements from the other set of facts. It suffices to argue that if Spoiler changes the active set like this, and chooses no new elements, then the game is still in a safe position. But in this case f 0 = f 1 is easily seen to still be safe.

This concludes the proof of Proposition 7.

We can now conclude the proof of Proposition 1. Assume that F ◆ F 0 is a set of facts that satisfies ' when interpreting R + as the transitive closure of R. Let 3  k  |'| be an upper bound on the maximum number of free variables in any subformula of '. Since F satisfies ', Propositions 7 and 6 imply that F k also satisfies ' when properly interpreting R + . Hence, we can conclude that the unravelling F k is the transitive closure friendly k-tree-like witness for '.

C Automata for BaseGNF (Proof of Theorem 2)

In this section, we prove Theorem 2, about constructing automata for sentences in BaseGNF and initial sets of facts F 0 : Theorem 2. Let ' be a sentence in BaseGNF, and let F 0 be a finite set of facts. We can construct in 2EXPTIME a 2-way alternating parity tree automa-

ton A ',F0 such that F 0 ^' is satisfiable iff L(A ',F0 ) 6 = ; when R + 2 D are interpreted as the transitive clo- sure of R 2 B . The number of states of A ',F0 is exponential in |'|•|F 0 | and the number of priorities is linear in |'|.
Before we prove the result, we need to specify the tree encodings/decodings and tree automata that we are using. For the remainder of the section, we fix some ' 2 BaseGNF and some finite set of facts F 0 .

C.1 Tree encodings/decodings

Tree encodings. By Proposition 1, we know that if ' 2 BaseGNF, then ' has transitive-closure friendly k-tree-like witnesses, for k  |'|. A F 0 -rooted tree decomposition like this can be encoded as a tree with only a finite signature. Let U be a set of names of size 2k + l where l is the size of elems(F 0 ). The signature ˜ k for the encodings is defined as follows.

• For all a 2 U , there is a unary relation D a 2 ˜ k which indicates that a is a name for an element represented in the bag.

• For every relation R 2 of arity n and every n-tuple

ã 2 U n
, there is a unary relation R ã 2 ˜ k , which indicates that R holds for the tuple of elements indexed by ã.

• For every z 2 elems(F 0 ) and c 2 U , there is a unary relation V c/z which indicates the valuation for this element. Tree decompositions and the corresponding encodings can generally have unbounded (possibly infinite) degree. We modify the standard encoding slightly so that we can use full binary trees: we apply the first-child, next-sibling transformation to the usual encoding, based on an arbitrary ordering of the children, and make it a full binary tree by adding dummy nodes if necessary.

Each node in a binary tree can be identified with a finite string over {0, 1}, with the root identified with ✏. The biological children of a node u are the nodes u01 + (these are the nodes that would have been children of u in the tree decomposition before the first-child next-sibling translation). The biological parent of v 6 = ✏ is the unique u such that v 2 u01 + . A biological neighbor is a biological child or biological parent.

For these binary tree encodings, we add to ˜ k unary predicates P i for i 2 {0, 1} which indicate the node is the i-th child of its parent.

From now on, we use the term ˜ k -tree to refer to an infinite full binary tree over the signature ˜ k .

Tree decodings. If a ˜ k -tree satisfies certain consistency properties, then it can be decoded into a set of -facts with an F 0 -rooted tree decomposition of width k 1. Let names(v) := {a 2 U : D a (v)} be the set of names used for elements in bag v in some tree. We will abuse notation and write ã ✓ names(v) to mean that ã is a tuple over names from names(v). A consistent tree T (with respect to ˜ k and F 0 ) is a ˜

k -tree such that every node v satisfies • |names(v)|  k, except for the root (which has size l);

• for all R ã 2 ˜ k , if R ã (v) then ã ✓ names(v); • P i (v) holds iff v is the i-th child of its parent; • for all z 2 elems(F 0 ), there is exactly one c 2 names(✏)
for the root ✏ such that V c/z (✏) holds, and there is no v 6 = ✏ with some c 2 names(v) such that V c/z (✏) holds; • for every c 2 names(✏), there is some z 2 elems(F 0 )

such that V c/z (✏) holds; • for each fact R(z 1 . . . z n ) 2 F 0 , R c1...cn (✏) holds, where each c i 2 names(✏) is the unique name such that V ci/zi (✏) holds; • for every R c1...cn (✏), the fact R(z 1 . . . z n ) is in F 0 , where each z i 2 elems(F 0 ) is the unique element such that V ci/zi (✏)
holds. The last four conditions ensure that there is a bijection between the elements and facts represented at the root node and the elements and facts in F 0 .

Given a consistent tree T , we say nodes u and v are a-connected if there is a sequence of nodes u = w 0 , w 1 , . . . , w j = v such that w i+1 is a biological neighbor of w i , and a 2 names(w i ) for all i 2 {0, . . . , j}. We write [v, a] for the equivalence class of a-connected nodes of v. For

✏, c] such that V c/z (✏) holds. For each relation R, we have R([v 1 , a 1 ], . . . , [v j , a j ]) 2 decode(T ) iff there is some w 2 T such that R ã (w) holds and [w, a i ] = [v i , a i ] for all i.
Free variables. The automaton construction will be an induction on the structure of the formula, so we will need to deal with formulas with free variables. For this purpose, the tree encodings can be extended with additional information about valuations for free variables. Such trees use an extended signature.

Namely, for each free first-order variable z and each c 2 U , we introduce a predicate V c/z ; if V c/z (v) holds, then this indicates that the valuation for z is the element named by c at v (we use notation similar to the valuations for z 2 elems(F 0 ), since these valuations all behave in a similar way).

At one point in what follows (specifically, in one case of the proof of Lemma 3), we will also use second-order variables to represent information about some additional relation Y .

For each second-order variable Y of arity n and each ã 2 U n , the extended signature has a predicate Y ã . If Y ã holds at some node v, then this indicates that the tuple of elements indexed by ã at v is in the relation Y .

We refer to these additional predicates that give a valuation for the free variables as free variable markers. In a consistent tree, the free variables markers for a first-order variable z must satisfy the condition that there is a unique v and unique c 2 names(v) such that V c/z (v) holds (i.e. for each z there is exactly one V c/z -fact in the tree). The markers for a secondorder variable Y must satisfy the condition that if Y ã (v) then ã ✓ names(v).

C.2 Automata tools

We will make use of automata running on infinite binary trees. We briefly recall some definitions and key properties. We will need to use 2-way automata that can move both up and down as they process the tree, so we highlight some less familiar properties about the relationship between 2-way and 1-way versions of these automata.

Trees. The input to the automata will be infinite full binary trees T over some finite set of propositions . In other words, these are structures over a signature with binary relations for the left and right child relation, and unary relations for the propositions. We also assume there are propositions indicating whether each node is a left child, right child, or the root. We write T (v) for the set of propositions that hold at node v.

Tree automata. An alternating parity tree automaton A is a tuple h , Q, q 0 , , ⌦i where is a finite set of propositions, Q is a finite set of states, q 0 2 Q is the initial state,

: Running the automaton A on some input tree T is best thought of in terms of an acceptance game. Positions in the game are of the form (q, v) 2 Q ⇥ T . In position (q, v), Eve chooses a disjunct ✓ in 0 (q, T (v)), where 0 is the result of writing each of the transition function formulas in disjunctive normal form. Then Adam chooses a conjunct (d, q 0 ) in ✓ and the game continues from position (q 0 , v 0 ), where v 0 is the node in direction d from v (Adam loses if there is no such node v 0

Q ⇥ P( ) ! B + (Dir ⇥ Q) is
). A play (q 0 , v 0 )(q 1 , v 1 ) . . . in the game is winning for Eve if it satisfies the parity condition: the maximum priority occurring infinitely often in ⌦(q 0 )⌦(q 1 ) . . . is even. A strategy for Eve is a function that, given the history of the play and the current position in the game, determines Eve's choice in the game. Note that we allow the automaton to be started from arbitrary positions in the tree, rather than just the root. We say that A accepts T starting from v 0 if Eve has a strategy such that all plays consistent with the strategy starting from (q 0 , v 0 ) are winning. L(A) denotes the language of trees accepted by A starting from the root.

A 1-way alternating automaton is an automaton that uses only directions 0 and 1. A (1-way) nondeterministic automaton is a 1-way alternating automaton such that every transition function formula is of the form W j (0, q j 0 ) ^(1, q j 1 ).

Closure properties. We recall some closure properties of these automata, omitting the standard proofs; see [START_REF] Thomas | Wolfgang Thomas. Languages, Automata, and Logic[END_REF]Löding, 2011] for more information. Note that we state only the size of the automata for each property, but the running time of the procedures constructing these automata is polynomial in the output size.

First, the automata that we are using are closed under union and intersection (of their languages). Proposition 8. 2-way alternating parity tree automata and 1way nondeterministic parity tree automata are closed under union and intersection, with only a polynomial blow-up in the number of states, priorities, and overall size.

For example, this means that if we are given 2-way alternating parity tree automata A 1 and A 2 , then we can construct in PTIME a 2-way alternating parity tree automaton A such that

L(A) = L(A 1 ) \ L(A 2 ).
Another important language operation is projection. Let L 0 be a language of trees over propositions [{P }. The projection of L 0 with respect to P is the language of trees T over such that there is some T 0 2 L 0 such that T and T 0 agree on all propositions in . Projection is easy for nondeterministic automata since the valuation for the projected proposition can be guessed by Eve. Proposition 9. 1-way nondeterministic parity tree automata are closed under projection, with no change in the number of states, priorities, and overall size.

Finally, complementation is easy for alternating automata by taking the dual automaton, obtained by switching conjunctions and disjunctions in the transition function, and incrementing all of the priorities by one. Proposition 10. 2-way alternating parity tree automata are closed under complementation, with no change in the number of states, priorities, and overall size.

Connections between 2-way and 1-way automata. It was shown by Vardi [1998] that 2-way alternating parity tree automata can be converted to equivalent 1-way nondeterministic automata, with an exponential blow-up. Theorem 11 ( [Vardi, 1998]). Let A be a 2-way alternating parity tree automaton. We can construct a 1-way nondeterministic parity tree automaton A 0 such that L(A) = L(A 0 ). The number of states of A 0 is exponential in the number of states of A, but the number of priorities of A 0 is linear in the number of priorities of A.

1-way nondeterministic tree automata can be seen as a special case of 2-way alternating automata, so the previous theorem shows that 1-way nondeterministic and 2-way alternating parity automata are equivalent, in terms of their ability to recognize trees starting from the root.

We need another conversion from 1-way nondeterministic to 2-way alternating automata that we call localization. This is the process by which a 1-way nondeterministic automaton that is running on trees with extra information about some predicate annotated on the tree is converted to an equivalent 2-way alternating automaton that operates on trees without these annotations under the assumption that these predicates hold only locally at the position the 2-way automaton is launched from. A similar localization theorem is present in prior work [START_REF] Bourhis | [END_REF]Benedikt et al., 2016]. Theorem 12. Let 0 := [ {P 1 , . . . , P j }. Let A 0 be a 1way nondeterministic parity automaton on 0 -trees. We can construct a 2-way alternating parity automaton A on -trees such that for all -trees T and nodes v 2 Dom(T ), A 0 accepts T 0 from the root iff A accepts T from v where T 0 is the 0 -tree obtained from T by setting

P T 0 1 = • • • = P T 0 j = {v}.
The number of states of A is linear in the number of states of A 0 , and the overall size of A is linear in the size of A 0 . The number of priorities of A is linear in the number of priorities of A 0 . Proof sketch. A simulates A 0 by guessing in a backwards fashion an initial part of a run of A 0 on the path from v to the root and then processing the rest of the tree in a normal downwards fashion. The subtlety is that the automaton A is reading a tree without valuation for P 1 , . . . , P j so once the automaton leaves node v, if it were to cross this position again, it would be unable to correctly simulate A 0 . To avoid this issue, we only send downwards copies of the automaton in directions that are not on the path from the root to v.

Emptiness testing. Finally, we make use of the well-known fact that language emptiness of tree automata is decidable. Theorem 13 ( [START_REF] Emerson | [END_REF], [Vardi, 1998]). For 1-way nondeterministic parity tree automata, emptiness is decidable in time polynomial in the number of states and exponential in the number of priorities. For 2-way alternating parity automata, it is decidable in time exponential in the number of states and priorities.

C.3 Construction

We are almost ready to construct an automaton for ' 2 BaseGNF and F 0 to prove Theorem 2. It is convenient to work with normal form formulas, so let ' 0 be the normal form BaseGNF sentence that is equivalent to '.

We build up this automaton inductively, so we must construct an automaton A for each subformula (x) of ' 0 . The automaton A will not specify a single initial state. Instead, there will be a designated initial state for each possible "local assignment" for the free variables x. A local assignment ã/x for ã = a 1 . . . a n 2 U n and x = x 1 . . . x n is a mapping such that x i 7 ! a i . A node v in a consistent tree T with ã ✓ names(v) and a local assignment ã/x, specifies a valuation for x. We say it is local since the free variable markers for x would all appear locally in v.

We will write A for the automaton for (without specifying the initial state), and will write A ã/x for A with the designated initial state for ã/x. We call A ã/x a localized automaton, since it is testing whether some tuple that is represented locally in the tree satisfies . Localized automata are useful because they can be launched to test that a tuple of elements that appear together in a node satisfy some propertywithout having the markers for this tuple explicitly written on the tree.

The construction is described in the following lemma. Lemma 3. Let (x) be a subformula of ' 0 (the normal form version of '). Let k be the width of ' 0 , let l be the size of elems(F 0 ), and let K := 2k + l.

We can construct a 2-way alternating parity tree automaton A such that for all consistent trees T , for all local assignments ã/x, and for all nodes v in T with ã ✓ names(v),

A ã/x accepts T starting from v iff decode(T ), [v, ã] satisfies when each R + 2 D is interpreted as the transitive closure of R 2 B .
Further, there is a polynomial function f independent of such that the number of states of A is at most Kr ) where m = | | and r is the CQ-rank of . The overall size of the automaton and the running time of the construction is at most exponential in | | • N . The number of priorities is linear in .

N := f (m ) • 2 f (
Proof. We proceed by induction on normal form (x) in BaseGNF. We will write m for | |, r for the CQ-rank of , and N for f (m ) • 2 f (Kr ) for some suitably chosen (in particular, non-constant) polynomial f independent of (we will not define f explicitly).

During each case of the inductive construction, we will describe informally how to build the desired automaton, and we will analyze the number of priorities and the number of states required. We defer the analysis of the overall size of the automaton until the end of this proof.

Base cases. For each of the base cases (x), we first describe a 2-way alternating parity tree automaton B that runs on trees with the free variable markers for x written on the tree:

• Suppose is a B -atom ↵(x). Eve tries to navigate to a node v whose label includes fact ↵( b). If she is able to do this, Adam can then challenge Eve to show that x corresponds to b. Say he challenges her on b i 2 b. Then Eve must navigate from v to the node carrying the marker b i /x i . However, she must do this by passing through a series of biological neighbors that also contain b i (the intermediate nodes in between biological neighbors might not contain b i ). If she is able to do this, B enters an accepting sink state (with priority 0). The other states are non-accepting (with priority 1) to ensure that Eve actually witnesses ↵(x). The number of states of B is linear in K, since the automaton must remember the name b i that Adam is challenging. There are two priorities.

• The case when is the B -guardedness predicate guarded B (x) is similar, except Eve can choose any atom ↵ over B that uses all of the variables x, and then proceed as in the previous case.

• Suppose is an equality x 1 = x 2 . Eve navigates to the node v with the marker a/x 1 . She is then required to navigate from v to the node carrying the marker for x 2 . She must do so by passing through a series of biological neighbors that also contain a (again, the intermediate nodes in between biological neighbors might not contain a). If she is able to reach the marker a/x 2 in this way then x 1 and x 2 are marking the same element in the underlying set of facts, so B moves to a sink state with priority 0 and she wins. The other states have priority 1, so if Eve is not able to do this, then Adam wins. The state set is of size linear in K, in order to remember the name a. There are two priorities.

• Suppose is a D -atom R + (x 1 , x 2 ). Eve first tries to navigate to the node v 0 carrying the marker a 1 /x 1 for x 1 . The automaton B then simulates the following game. The initial position in the game is (v 0 , a 1 ). In general, positions in the game are of the form (v, a) for a node v and a name a, and one round of the game consists of the following: Eve can either choose a 0 in v such that label at v includes fact R(a, a 0 ); she immediately wins if v includes marker a 0 /x 2 , otherwise she proceeds to the next round in position (v, a 0 ), or choose some biological neighbor v 0 which includes the name a, and the game proceeds to the next round in position (v 0 , a). This game can be implemented using a 2-way automaton. Winning corresponds to moving to a sink state with priority 0. All of the other states are assigned priority 1. This ensures that eventually Eve witnesses a path of Rfacts from x 1 to x 2 . The number of states in B is again linear in K, since it must remember the name a that is currently being processed along this path. There are only two priorities. For each base case (x), we have constructed an automaton B with two priorities and a state set of size linear in K.

However, this automaton runs on trees with the free variable markers for x, so it remains to show that we can construct the automaton A required by the lemma that runs on trees without these markers.

First, we can convert B into an equivalent nondeterministic parity tree automaton with an exponential blow-up in the number of states and a linear blow-up in the number of priorities (using Theorem 11). After this step, the number of states is exponential in K.

For each local assignment ã/x, we can then apply the localization theorem (Theorem 12) to the set of predicates of the form V ai/xi , and eliminate the dependence on any other V c/xi for c 6 = a i by always assuming these predicates do not hold. This results in a localized automaton A ã/x that no longer relies on free variable markers for x. By Theorem 12, there is only a linear blow-up in the number of states and number of priorities, so after this step the number of states in each A ã/x is exponential in K.

Finally, we take A to be the disjoint union of A ã/x over all local assignments ã/x; the designated initial state for each localization is the initial state for A ã/x . Since there are at most K k localizations, the number of states in A is still exponential in K, which can be assumed to be less than N by the choice of f . The number of priorities is a constant independent of .

Inductive cases. We now proceed with the inductive cases.

We build A with the help of inductively defined automata for its subformulas.

• Suppose is a guarded negation of the form ↵(x) ¬ 0 (x). Construct A by taking the disjoint union of A ↵ , the dual of A 0 (obtained by switching conjunctions and disjunctions in the transition function formulas in A 0

, and incrementing each priority by one), and fresh states q ã/x with priority 1 for each local assignment ã/x. For each local assignment ã/x, the designated initial state is q ã/x . From state q ã/x , Adam is given a choice whether to move to the initial state of A ã/x ↵ or to the initial state of the dual of A ã/x 0 . The idea is that Adam selects which of the conjuncts to challenge Eve on. The state set of A is of size at most Kr ) f (m ↵ + m 0 + 1)  N . The number of priorities is linear in the size of , since it is at most the sum of the number the priorities in the subautomata for ↵ and 0 (which by the inductive hypothesis were linear in the size of these subformulas).

f (m ↵ ) • 2 f (Kr↵) + f (m 0 ) • 2 f (Kr 0 ) + K k  2 f (Kr ) (f (m ↵ ) + f (m 0 ) + 1)  2 f (
• Suppose is a disjunction 1 _ • • • _ s . Construct A by taking the disjoint union of the A i and fresh states q ã/x with priority 1 for each local assignment ã/x. For each local assignment ã/x, the designated initial state is q ã/x . In state q ã/x , Eve chooses which A ã/x i to simulate. The number of states of A is at most

f (m 1 ) • 2 f (Kr 1 ) + • • • + f (m s ) • 2 f (Kr s ) + K k  2 f (Kr ) (f (m 1 ) + • • • + f (m s ) + 1)  2 f (Kr ) f (m 1 + • • • + m s + 1)  N .
The number of priorities is linear in the size of , since it is at most the sum of the number of priorities in the subautomata for 1 to s (which by the inductive hypothesis were linear in the size of these subformulas).

• Suppose (x) is a CQ

9y 1 . . . y t (↵ 1 (z 1 ) ^• • • ^↵s (z s ))
where each zi is a tuple of variables coming from x and y 1 , . . . , y t , and each ↵ i is an atom over B [ D . This is a specific case, but it is helpful for handling the general CQ-shaped formulas in the next point. We start by defining an automaton that runs on trees with free variable markers for x and y 1 . . . y t . For 1  i  s, let B ↵i be the automaton for ↵ i described in the base cases above that runs on trees with the free variable markers for x and y 1 . . . y t . Let C be the automaton obtained by taking the disjoint union of B ↵1 , . . . , B ↵s , and an automaton checking that there is precisely one free variable marker for y 1 . . . y t , and adding a new initial state with priority 1 from which Adam can choose which of these subautomata to simulate. Thus, C is a 2-way alternating automaton with number of states linear in Ks  Kr , and two priorities; it checks that the body of the CQ holds in a tree with all of the free variable markers present. We can then convert C to an equivalent nondeterministic parity tree automaton C 0 using Theorem 11, with an exponential blow-up in the number of states, and a linear blow-up in the number of priorities. After this step, the number of states is exponential in Kr . Next, we take the projection of C 0 on the free variable markers for y 1 . . . y t to obtain B : that is, B simulates C 0 while guessing the markers for the variables y 1 . . . y t . This is an automaton for , but it runs on trees with markers for the free variables x. For each local assignment ã/x, we can then apply the localization theorem (Theorem 12) to the set of predicates of the form V ai/xi , and eliminate the dependence on any other V c/xi for c 6 = a i by always assuming these predicates do not hold. This results in a localized automaton A ã/x that no longer relies on free variable markers for x. By Theorem 12, there is only a linear blow-up in the number of states and number of priorities, so after this step the number of states is exponential in Kr .

Finally, we take A to be the disjoint union of the A ã/x over all local assignments ã/x; the designated initial state for each localization is the initial state for A ã/x . Since there are at most K k localizations, the number of states in A is still exponential in Kr , which can be assumed to be less than N by the choice of f . The number of priorities is a constant independent of .

• Suppose is a CQ-shaped formula of the form

[Y 1 := ' 1 , . . . , Y n := ' n ]
where is a CQ over [ {Y 1 , . . . , Y n } and ' i 2 BaseGNF. The inductive hypothesis yields A 'i for each of the ' i . Let N be the automaton for the CQ obtained using a similar approach as the previous case. Note that this automaton runs on trees with a valuation for the free second-order variables Y i marked on the tree. These free variables represent base-guarded relations (i.e. relations in which each tuple in the relation is base-guarded), since it is guaranteed that for each Y i atom, there is a Batom or B -guardedness predicate in that contains its free variables.

To construct A , take the disjoint union of N , A '1 , . . . A 'n . For each localization ã/x, the designated initial state is the initial state for ã/x coming from N . The idea is that A starts by simulating N , but with Eve guessing valuations for Y i . This is where it is important that the Y i are B -guarded relations: since any Y i -fact must be about a B -guarded set of elements, these elements must appear together in some node of the tree, so Eve can guess an annotation of the tree that indicates that Y i holds of these elements. Adam can either accept Eve's guesses of the valuation and continue the simulation of N , or can challenge one of Eve's assertions of Y i by launching the appropriate localized version of ' i . That is, if Eve guesses that Y i (z i ) holds of b at v, then Adam could challenge this by launching A b/zi 'i starting from v. This is where it is crucial that we have localized automata for these subformulas and for all possible local assignments that can be launched from internal nodes when Adam challenges one of Eve's guesses: in particular, note that the same A b/zi 'i can be launched for different initial localizations ã/x. By the inductive hypothesis, each A 'i automaton has at most f (m

'i ) • 2 f (Kr' i )
states, and number of priorities linear in m 'i . Likewise, the automaton N for has two priorities and number of states exponential in Kr , which we can assume to be at most at most 2 f (Kr ) . Hence, the number of priorities in A is linear in m , and the number of states in A is at most

2 f (Kr ) + f (m '1 ) • 2 f (Kr' 1 ) + . . . + f (m 'n ) • 2 f (Kr' n )  2 f (Kr ) (1 + f (m '1 ) + • • • + f (m 'n ))  N .
This concludes the inductive cases. It can be checked that the running time of the construction is polynomial in the size of the constructed automaton, and hence is also exponential in | | • N .

We must also construct an automaton that checks that the input tree is consistent, and actually represents a set of facts F such that F ◆ F 0 and where every R + -fact in F 0 is actually witnessed by some path of R-facts in F. For notational simplicity in the statement of the lemma, we assume that the element names in F 0 are used as the names in U for the root of the consistent trees (but this is only a technicality). Proof. The automaton is designed to allow Adam to challenge some consistency condition or a particular fact S(c) in F 0 .

It is straightforward to design suitable automata checking each consistency condition, so suppose Adam challenges some fact in F 0 . Then the automaton simply launches A c/x S(x) (obtained from Lemma 3) from the root. Note that in case S(c) is some R + (c 1 , c 2 ), this R-path witnessing this fact may require elements outside of elems(F 0 ) even though c 1 and c 2 are names of elements in F 0 .

The number of states is exponential in | |•K, and the overall size is at most doubly exponential in | | • K. Only two priorities are needed.

We can now conclude the proof of Theorem 2. Recall that ' is in BaseGNF and F 0 is some finite set of facts. Without loss of generality, we can assume that

|'| • |F 0 | | |.
We construct the normal form ' 0 equivalent to ' in exponential time using Proposition 5. Although the size of ' 0 can be exponentially larger than ', the width and CQ-rank is at most |'|, so we can apply Lemma 3 to construct an automaton for ' 0 (and hence ') in time doubly exponential in |'| • |F 0 |. However, the number of states and priorities in this automaton is at most singly exponential in |'| • |F 0 |, and the number of priorities is linear in |'|. By taking the intersection of this automaton from Lemma 3 with the automaton for F 0 and consistency from Lemma 4, we have a 2-way alternating parity tree automaton A ',F0 of the desired size that has a non-empty language iff ' is satisfiable. This concludes the proof of Theorem 2.

D Base-guarded-interface tree decompositions for BaseGNF

We prove the following result: Proposition 11. Every sentence ' in BaseGNF has baseguarded-interface k-tree-like witnesses for some k  |'|.

That is, for every sentence ' in BaseGNF and for every finite set of facts F 0 , if there is some F ◆ F 0 satisfying ' then there is such an F that has a F 0 -rooted (k 1)-width base-guarded-interface tree decomposition.

The result and proof of Proposition 11 is very similar to Proposition 1. However, unlike Proposition 1, we do not interpret the distinguished relations in a special way here. This allows us to prove the stronger base-guarded-interface property about the corresponding tree decompositions, which will be important for later arguments (e.g., Proposition 3 and Theorem 4).

We first consider a variant of the GN k bisimulation game defined earlier in Appendix B. The positions in the game are the same as before:

i) partial isomorphisms f : F X ! G Y or g : G Y ! F
X , where X ⇢ elems(F) and Y ⇢ elems(G) are both finite and are B -guarded;

ii) partial rigid homomorphisms f :

F X ! G Y or g : G Y ! F X ,
where X ⇢ elems(F) and Y ⇢ elems(G) are both finite and are of size at most k.

However, the rules of the game are different. From a type (i) position h, Spoiler must choose a finite subset X ⇢ elems(F) or a finite subset Y ⇢ elems(G), in either case of size at most k, upon which Duplicator must respond by a partial rigid homomorphism with domain X or Y accordingly, mapping it into the other set of facts in a manner consistent with h. (This is the same as before).

In a type (ii) position h, Spoiler is only allowed to select some base-guarded subset X 0 of Dom(h), and then the game proceeds from the type (i) position obtained by restricting h to this base-guarded subset.

Thus, the game strictly alternates between type (ii) positions and base-guarded positions of type (i). We call this a base-guarded-interface GN k bisimulation game, since the interfaces (i.e. shared elements) between the domains of consecutive positions must be base-guarded. We can then show: Proposition 12. Let ' 2 BaseGNF k in normal form.

If Duplicator has a winning strategy in the base-guardedinterface GN k bisimulation game between F and G starting from a type (i) position ã 7 ! b and F satisfies '(ã), then G satisfies '( b).

Proof. Suppose Duplicator has a winning strategy in the base-guarded-interface GN k bisimulation game between F and G.

If ' is a -atom A(x), the result follows from the fact that the position ã 7 ! b is a partial homomorphism.

If ' is a disjunction, the result follows easily from the inductive hypothesis.

Suppose ' is a base-guarded negation A(x) ^¬' 0 (x 0 ). By definition of BaseGNF, it must be the case that A 2 B and x0 is a sub-tuple of x. Since F,ã satisfies ', we know that F,ã satisfies A(x), which implies (by induction) that G, b also satisfies A(x). It remains to show that G satisfies ¬' 0 (x 0 ). Assume for the sake of contradiction that it satisfies ' 0 (x 0 ). Because ã 7 ! b is a type (i) position, we can consider the move in the game where Spoiler switches the domain to the other set of facts, keeps the same set of elements, and then collapses to the base-guarded elements in the subtuple b0 of b corresponding to x0 in x. Let ã0 be the corresponding subtuple of ã. Duplicator must still have a winning strategy from this new type (i) position b0 7 ! ã0 , so the inductive hypothesis ensures that F,ã 0 satisfies ' 0 (x 0 ), a contradiction. Finally, suppose ' is a CQ-shaped formula

[Y 1 := ' 1 , . . . , Y n := ' n ]
where is a CQ 9ỹ(↵

1 ^• • • ^↵j ) over [ {Y 1 , . . . , Y n } and ' i is in normal form BaseGNF k
. We are assuming that F,ã satisfies '. Hence, there is some c 2 elems(F) such that

F,ã, c satisfies (↵ 1 ^• • • ^↵j )[Y 1 := ' 1 , . . . , Y n := ' n ].
Because the width of ' is at most k, we know that the combined number of elements in ã and c is at most k. Hence, we can consider the move in the game where Spoiler selects the elements in ã and c. Duplicator must respond with some d 2 elems(G) such that ãc 7 ! b d is a partial rigid homomorphism, a type (ii) position. Now consider the possible conjuncts in this CQ-shaped formula. Conjuncts that are -atoms must be satisfied in G, b d since ãc 7 ! b d is a partial homomorphism with respect to . For the conjuncts ' i corresponding to Y i , we can consider Spoiler's restriction of ãc to the elements used by this conjunct, and the corresponding restriction of b d. This is a valid move to a type (i) position, since the definition of BaseGNF requires that these non-atomic conjuncts are base-guarded. Moreover, this new position witnesses the satisfaction of that conjunct in F. Since Duplicator must still have a winning strategy from this new type (i) position, the inductive hypothesis implies that this conjunct is also satisfied in G. Since this is true for all conjuncts in the CQ-shaped formula, G, b satisfies ' as desired.

We then use a variant of the unravelling based on this game. The base-guarded-interface GN k -unravelling F k B is defined in a similar fashion to the GN k -unravelling, except it uses only sequences ⇧ \ {X 0 . . . X n : for all i 1, X i \ X i+1 is B -guarded}. This unravelling has an F 0 -rooted base-guarded-interface tree decomposition of width k 1. Moreover: Proposition 13. Duplicator has a winning strategy in the base-guarded-interface GN k bisimulation game between F and F k B . Proof. The proof is similar to Proposition 7. The delicate part of the argument is when Spoiler selects some new elements X 0 in F starting from a safe position f (for which there is some ⇡ such that f (a) = [⇡, a] for all a 2 Dom(f )). We need to show that [⇡ 0 , a 0 ] for a 0 2 X 0 and ⇡ 0 = ⇡ • X 0 is well-defined in F k B . This is well-defined only if the overlap between the elements in ⇡ and ⇡ 0 is base-guarded. But because the base-guarded-interface GN k bisimulation game strictly alternates between type (i) and (ii) positions, Spoiler can only select new elements X 0 in a type (i) position, so the overlap satisfies this requirement. The remainder of the proof is the same as in Proposition 7.

We can conclude the proof of Proposition 11 as follows. Assume that F is a set of facts that satisfies '. By Proposition 5, we can convert to an equivalent ' 0 2 BaseGNF k in normal form with width k  |'|. Since F satisfies ' 0 , Propositions 13 and 12 imply that F k B also satisfies ' 0 2 BaseGNF k

. Hence, we can conclude that the unravelling F k B is a base-guarded-interface k-tree-like witness for '.

E Reduction of QAlin to QA (Proof of Lemmas 1 and 2 for Proposition 3)

Recall the statement of Proposition 3, which describes the reduction from QAlin to QA: Proposition 3.

For any finite set of facts F 0 , constraints ⌃ 2 BaseCovGNF, and base-covered UCQ Q, we can compute F 0

0 and ⌃ 0 2 BaseGNF in PTIME such that QAlin(F 0 , ⌃, Q) iff QA(F 0 0 , ⌃ 0 , Q).
Specifically, F 0 0 is F 0 together with facts G(a, b) for every pair a, b 2 elems(F 0 ), where G is some fresh binary base relation. ⌃ 0 consists of ⌃ together with the k-guardedly linear axioms for each distinguished relation, where k is max(|⌃ ¬Q|, arity( [ {G})).

Recall that the k-guardedly linear axioms require that each binary relation < is:

• guardedly total: 8xy((guarded B [{G} (x, y)^x 6 = y) ! x < y _y < x)

• irreflexive: ¬9x(x < x)

• k-guardedly transitive: for 1  l  k 1: ¬9xy( l (x, y) ^guarded B [{G} (x, y) ^¬(x < y)) and, for 1  l  k: ¬9x( l (x, x) ^x = x ^¬(x < x)) where:

• guarded B [{G} (x, y) is the formula expressing that x, y is base-guarded (an existentially-quantified disjunction over all possible base-guards containing x and y); • 1 (x, y) is just x < y; and

• l (x, y) for l 2 is: 9x 2 . . . x l (x < x 2 ^• • • ^xl < y).
The idea is that these axioms are strong enough to enforce conditions about transitivity and irreflexivity within "small" sets of elements -intuitively, within sets of at most k elements that appear together in some bag of a (k 1)-width tree decomposition.

The proof of the correctness of the reduction is described in the body of the paper, but relies on Lemmas 1 and 2, which we prove now.

E.1 Proof of Lemma 1

Recall the statement:

Lemma 1. The sentence ⌃ 0 ^¬Q has base-guardedinterface k-tree-like witnesses for k = max(|⌃ ¬Q|, arity( [ {G})).

By Proposition 5 and Proposition 11, ⌃ ^¬Q has a baseguarded-interface k-tree-like witness for k = |⌃ ^¬Q|.

To prove this lemma, then, it suffices to argue that the k-guardedly linear axioms can also be written in normal form BaseGNF with width at most k.

The guardedly total axiom is written in normal form BaseGNF as

¬9xy(guarded B [{G} (x, y) ^¬(x = y _ x < y _ y < x))
with width at most k. The irreflexive axiom is already written in normal form BaseGNF with width at most k. For the k-guardedly transitive axioms, note that l (x, y) has width l + 1 and l (x, x) has width l, so that each of the k-guardedly transitive axioms has width at most k: this uses the fact that the width of the guarded B [{G} -atoms have arity at most arity( [ {G}), and we know that k arity( [ {G})

Therefore, unlike the property of being a linear order, the k-guardedly linear restriction can be expressed in BaseGNF, and can even be written in normal form BaseGNF of width at most k. Overall, this means that if ⌃ ^¬Q has width at most k when converted into normal form then ⌃ 0 ^¬Q also has width at most k. Hence, the sentence ⌃ 0 ^¬Q has baseguarded-interface k-tree-like witnesses for k = |⌃ ^¬Q|, by Proposition 11.

E.2 Proof of Lemma 2

Recall the statement:

Lemma 2. If there is F 0 ◆ F 0 0 that satisfies ⌃ 0 ^¬Q and has a F 0 0 -rooted base-guarded-interface (k 1)-width tree decomposition, then there is F 00 ◆ F 0 that satisfies ⌃ 0 ^¬Q where each distinguished relation is a strict linear order. We start with some auxiliary lemmas about base-guardedinterface tree decompositions.

Transitivity lemma. We first prove a result about transitivity for sets of facts with base-guarded-interface tree decompositions. Lemma 5. Suppose F 0 is a set of facts with a F 0 0 -rooted (k 1)-width base-guarded-interface tree decomposition (T, Child, ). If F 0 is k-guardedly transitive with respect to binary relation <, and there is a <-path a 1 . . . a n where the pair {a 1 , a n } is base-guarded, then a 1 < a n 2 F 0 . Proof. Suppose there is an <-path a 1 . . . a n and that the pair {a 1 , a n } is base-guarded, with v a node where a 1 , a n appear together. We can assume that a 1 . . . a n is a minimal <-path between a 1 and a n , so there are no repeated intermediate elements. Consider a minimal subtree T 0 of T containing v and containing all of the elements a 1 . . . a n . We proceed by induction on the length of the path and on the number of nodes of T 0

(with the lexicographic order on this pair) to show that a 1 < a n is in F 0 . If all elements a 1 . . . a n are represented at v, then either (i) all elements are in the root or (ii) the elements are in some internal node. For (i), by construction of F 0 0 , every pair of elements in a 1 . . . a n is guarded (by G). Hence, repeated application of the axiom 8xyz((x < z ^z < y ^guarded B [{G} (x, y)) ! x < y)

(which is part of the k-guardedly transitive axioms) is enough to ensure that a 1 < a n holds. For (ii), since the bag size of an internal node is at most k, we must have n  k, in which case an application of the k-guardedly transitive axiom to the guarded pair {a 1 , a n } ensures that a 1 < a n holds. This covers the base case of the induction.

Otherwise, there must be some 1  i < j  n such that a i and a j are represented at v, but a i 0

is not represented at v for i < i 0 < j (in particular a i+1 is not represented at v). We claim that a i and a j must be in an interface together. We say a i+1 is represented in the direction of v 0 if v 0 is a child of v and a i+1 is represented in the subtree rooted at v 0 , or v 0 is the parent of v and a i+1 is represented in the tree obtained from T 0 by removing the subtree rooted at v. Note that by definition of a tree decomposition, since a i+1 is not represented at v, it can only be represented in at most one direction.

Let v i+1 be the neighbor (child or parent) of v such that a i+1 is represented in the direction of v i+1 . It is straightforward to show that a i and a j must both be represented in the subtree in the direction of v i+1 in order to witness the facts a i < a i+1 and a j 1 < a j . But a i and a j are both in v, so they must both be in v i+1 . Hence, a i and a j are in the interface between v and v i+1 . If this is an interface with the root node, then the pair a i , a j is base-guarded (by definition of F 0 0 ). Otherwise, the definition of base-guarded-interface tree decompositions ensures that they are base-guarded.

Hence, we can apply the inductive hypothesis to the path a i . . . a j and the subtree T 00 of T 0 in the direction of v i+1 to conclude that a i < a j holds (we can apply the inductive hypothesis because T 00 is smaller than T 0 as we removed v, and a i . . . a j is no longer than a 1 . . . a n ). If i = 1 and j = n, then we are done. If not, then we can apply the inductive hypothesis to the new, strictly shorter path a 1 . . . a i a j . . . a n in T 0 and conclude that a 1 < a n is in F 0 as desired.

Cycles lemma. We next show that within base-guardedinterface tree decompositions, k-guarded transitivity and irreflexivity imply cycle-freeness. Lemma 6. Suppose F 0 is a set of facts with a F 0 0 -rooted (k 1)-width base-guarded-interface tree decomposition (T, Child, ). If F 0 is k-guardedly transitive and irreflexive with respect to <, then < in F 0 cannot have a cycle.

Proof. Suppose for the sake of contradiction that there is a cycle a 1 . . . a n a 1 in F 0 using relation <. Take a minimal length cycle.

If elements a 1 . . . a n are all represented in a single node in T , then either (i) all elements are in the root or (ii) the elements are in some internal node. For (i), by construction of F 0 0 , every pair of elements in a 1 . . . a n is guarded (by G). Hence, repeated application of the axiom 8xyz((x < z ^z < y ^guarded B [{G} (x, y)) ! x < y)

(which is part of the k-guardedly transitive axioms) would force a 1 < a 1 to be in F 0 , which would contradict irreflexivity. Likewise, for (ii), since the bag size of an internal node is at most k, we must have n  k, so we can apply the kguardedly transitive axioms to deduce a 1 < a 1 , which contradicts irreflexivity.

Even if this is not the case, then since a n < a 1 holds, there must be some node v in which both a 1 and a n are represented. Since not all elements are represented at v, however, there is 1  i < j  n such that a i and a j are represented at v, but a i 0 is not represented at v for i < i 0 < j. We claim that a i and a j must be in an interface together. Observe that a i+1 is not represented at v. Let v i+1 be the neighbor of v such that a i+1 is represented in the subtree in the direction of v i+1 . It is straightforward to show that a i and a j must both be represented in the subtree of T 0 in the direction of v i+1 in order to witness the facts a i < a i+1 and a j 1 < a j . But a i and a j are both in v, so they must both be in v i+1 . Hence, a i and a j are in the interface between v and v i+1 . If this is an interface with the root node, then the pair a i , a j is base-guarded (by definition of F 0 0 ); otherwise, the definition of base-guarded-interface tree decomposition ensures that they are base-guarded. By Lemma 5 this means that a i < a j holds. Hence, there is a strictly shorter cycle a 1 . . . a i a j . . . a n a 1 , contradicting the minimality of the original cycle.

Base-coveredness lemma. Lastly, we note that adding only facts about unguarded sets of elements cannot impact BaseCovGNF constraints. This is where we are utilizing the base-coveredness assumption. Lemma 7. Let F 00 ◆ F 0 with additional facts about distinguished relations, but no new facts about base-guarded tuples of elements. Let '(x) 2 BaseCovGNF. If F 0 ,ã satisfies '(x) then F 00 ,ã satisfies '(x).

Proof. We assume without loss of generality that ' is in normal form BaseCovGNF.

Let BaseCovGNF + (respectively, BaseCovGNF ) denote the normal form BaseGNF formulas where the covering requirements (distinguished atoms in CQ-shaped subformulas are appropriately base-guarded) are required for positively occurring (respectively, negatively occurring) CQ-shaped formulas. Observe that BaseCovGNF = BaseCovGNF .

We prove a slightly stronger result:

For '(x) 2 BaseCovGNF : F 0 ,ã satisfies '(x) implies F 00 ,ã satisfies '(x). For '(x) 2 BaseCovGNF + : F 00 ,ã satisfies '(x) implies F 0 ,ã satisfies '(x).

We proceed by induction on the structure of '. The base case for a B atom is immediate. The inductive case for disjunction is also immediate.

Suppose ' := A(x) ^¬' 0 (x), and ' 2 BaseCovGNF . If F 0 ,ã satisfies '(x), then F 00 ,ã satisfies A(x) by the inductive hypothesis. We must also have F 00

,ã satisfies ¬' 0 (x), for if not, then F 00 ,ã satisfies ' 0 (x) (for ' 0 2 BaseCovGNF + ), so the inductive hypothesis implies that F 0 ,ã satisfies ' 0 (x), a contradiction. Hence, F 00 ,ã satisfies '(x) as desired. The proof is similar starting from ' 2 BaseCovGNF + . That leaves only the general CQ-shaped formula case. Suppose '

:= 9ỹ ( 1 (x 1 ỹ1 ) ^• • • ^ j (x j ỹj ))
, where xi and ỹi denote the tuple of variables from x and ỹ used by i . If ' is in BaseCovGNF , then there are no covering restrictions for this CQ since it appears positively. If F 0 ,ã satisfies '(x), then there exists b, such that F 0 ,ã i bi satisfies i for all 1  i  j. But F 00 ◆ F 0 , so this witness b and the corresponding facts also appear in F 00

, and F 00 ,ã satisfies '. If ' is in BaseCovGNF + and F 00 ,ã satisfies ', then there is some b such that F 00 ,ã i bi satisfies i for all 1  i  j. It suffices to show that F 0 ,ã i bi satisfies i for all 1  i  j. Consider the possible i . If i is a B -atom, then F 0 ,ã i bi satisfies i , since F 0 has the same B -facts as F 00 . If i is a D -atom, then the covering requirements ensure that there is some Batom j in ' including at least the free variables xi ỹi of i . This means ãi bi is base-guarded. Since F 0 and F 00 agree on facts about base-guarded tuples like this, F 0 ,ã i bi satisfies i . Finally, if i is some structurally simpler BaseCovGNF formula, then the inductive hypothesis ensures that F 0 ,ã i bi satisfies i .

Final proof of Lemma 2. We are now ready to prove Lemma 2:

We start with some F 0 ✓ F 0 0 satisfying ⌃ 0 ^¬Q with a F 0 0rooted (k 1)-width base-guarded-interface tree decomposition. We prove that there is an extension F 00 of F 0 satisfying ⌃ 0 ^¬Q in which each distinguished relation is a strict linear order. Note that because F 0 satisfies ⌃ 0 , we know that F 0 is k-guardedly linear.

We present the argument when there is one < in D that is not a strict linear order in F 0 , but the argument is similar if there are multiple distinguished relations like this, as we can handle each distinguished relation independently with the method that we will present. Let G be the extension of F 0 obtained by taking < in G to be the transitive closure of < in F 0

. Suppose for the sake of contradiction that there is a <-cycle in G. We proceed by induction on the number of facts from G \ F 0 used in this cycle. If there are no facts from G \ F 0 in the cycle, Lemma 6 yields the contradiction. Otherwise, suppose that there is a cycle involving

(a 1 , a n ), where (a 1 , a n ) is a <-fact in G \ F 0 coming from facts (a 1 , a 2 ), . . . , (a n 1 , a n ) in F 0
. By replacing (a 1 , a n ) in this cycle with (a 1 , a 2 ), . . . , (a n 1 , a n ), we get a (longer) cycle with fewer facts from G \ F 0 , which is a contradiction by the inductive hypothesis.

Since < is transitive in G, the relation < in G must be a strict partial order. We now apply the "order extension principle" or "Szpilrajn extension theorem" [Szpilrajn, 1930]: any strict partial order can be extended to a strict total order. From this, we deduce that G can be further extended by additional <-facts to obtain some F 00

where < is a strict total order. We must prove that F 00 ◆ G ◆ F 0 ◆ F 0 0 does not include any new <-facts about base-guarded tuples. Suppose for the sake of contradiction that there is a new fact a < b in F 00 \F 0 , where {a, b} is base-guarded in F 0

. By the guardedly total axiom, it must be the case that there was already b < a in F 0 , and hence also in F 00

. But a < b and b < a in F 00 would together imply a < a in F 00

, contradicting the fact that F 00 is a strict linear order.

Hence, F 0 and F 00 agree on all facts about base-guarded tuples. Since Q is base-covered and ⌃ 2 BaseCovGNF, ⌃ ¬Q 2 BaseCovGNF. Thus, Lemma 7 guarantees that ⌃^¬Q is still satisfied in F 00

. Since F 00 also trivially satisfies all of the k-guardedly linear axioms, it satisfies ⌃ 0 ^¬Q as required. This concludes the proof of Lemma 2, and hence the proof of Proposition 3.

F Data complexity upper bounds for transitivity F.1 Proof of Theorem 3

We begin with the proof of Theorem 3. Recall the statement: Given an F, k-rooted structure A, and number j, the j-abstraction of A is the expansion of F with relations

P ⌧ (x 1 . . . x k ) for each FO( [ {d 1 . . . d k }
) sentence ⌧ of quantifier-rank j, up to logical equivalence (so there are finitely many such relations). P ⌧ (x 1 . . . x k ) is interpreted by the set of k-tuples c such that T c satisfies ⌧ when interpreting the constants in ⌧ by c. We let j,k be the signature of the j-abstraction of such structures. Lemma 8. For any sentence ' of FO( ) and any k, there is j having the following property:

Let A 1 be an F 1 , k-rooted structure for some set offacts F 1 , and let A 2 be an F 2 , k-rooted structure for some set of -facts F 2 , where the interpretations of the R + i relations in each structure are the transitive closure of the corresponding R i relations. If the j-abstractions of A 1 and A 2 agree on all FO( j,k ) sentences of quantifier-rank at most j, then A 1 and A 2 agree on '.

Proof. Let j

' be the quantifier-rank of '. We choose j • • = j ' • k. We give a strategy for Duplicator in the j ' -round standard pebble game for FO( ) over A 1 and A 2 . With i moves left to play, we will ensure the following invariants on a game position consisting of a sequence p1 2 A 1 and p2 2 A 2 :

• Let p1 0 be the subsequence of p1 that comes from F 1 and let p2 0 be defined similarly for p2 and F 2 . Then p1 0 and p2 0 should form a winning position for Duplicator in the i • k round FO( j,k ) game on the j-abstractions.

• Fix any k-tuple c1 2 F 1 and let P 1 c1 be the subsequence of p1 that lies in T c1 within A 1 . Then if P 1 c is non-empty, c1 also lies in p1 . Let c2 be the corresponding k-tuple to c1 in p2 , and let P 2 c2 be the subsequence of p2 that lies in T c2 within A 2 . Then P 1 c1 and P 2 c2 form a winning position in the i-round pebble game on T c1 and T c2 . The analogous property holds fixing any k-tuple c2 2 F 2 .

We now explain the strategy of the Duplicator, focusing for simplicity on moves of Spoiler within A 1 , with the strategy on A 2 being similar. If Spoiler plays within F 1 , Duplicator responds using her strategy for the games on the jabstractions of F 1 and F 2 . It is easy to see that the invariant is preserved.

If Spoiler plays an element within a substructure T c1 within A 1 that is already inhabited, then by the invariant c1 is pebbled and there is a corresponding c2 in A 2 with substructure T c2 of A 2 such that the pebbles within T c2 are winning positions in the game on T c1 and T c2 with i moves left to play. Thus Duplicator can respond using the strategy in this game from those positions. Now suppose Spoiler plays an element e 1 within a substructure T c1 within A 1 that is not already inhabited. We first use c1 as a sequence of plays for Spoiler in the game on the j-abstractions of A 1 and A 2 , extending the positions given by p1 0 and p2 0 . By the inductive invariant, responses of Duplicator exist, and we collect them to get a tuple c2 . Since a winning strategy in a game preserves atoms, and we have a fact in the j-abstraction corresponding to the j-type of c1 in T c1 , we know that c2 must satisfy the same j-type in T c2 that c1 does in T c1 . Therefore c1 must satisfy the same FO( [ {d 1 . . . d k }) sentences of quantifier-rank at most j in T c1 as c2 does in T c2 . Thus Duplicator can use the corresponding strategy to respond to e 1 with an e 2 in T c2 such that {e 1 } and {e 2 } are a winning position in the i 1 round pebble game on T c1 and T c2 . Since the response of Duplicator corresponds to k moves in the game within the j-abstractions, one can verify that the invariant is preserved.

We must verify that this strategy gives a partial isomorphism. Consider a fact F that holds of a tuple t1 within A 1 , and let t2 be the tuple obtained using this strategy in A 2 . We first consider the case where F is a B -fact.

• If t1 lies completely within some T c1 , then the last invariant guarantees that t2 lies in some T c2 . The last invariant also guarantees that B -facts of A 1 are preserved since such facts must lie in T c1 , and the corresponding positions are winning in the game between T c1 and T c2 . • If t1 lies completely within F 1 , then the first invariant guarantees that the fact is preserved.

By the definition of a rooted structure, the above two cases are exhaustive.

We now consider the case where F is of the form R + i (t 1 , t 2 ).

• If t 1 and t 2 both lie in some T c1 , then we reason as in the first case above.

• ⌃ 0
is ⌃ together with the k-guardedly-transitive axioms for each distinguished relation, where k is |⌃ ^¬Q|. These can be constructed in time polynomial in the size of the input.

As discussed in the proof of Lemma 1, the k-guardedly transitive axioms (see Appendix E) can be written in normal form BaseGNF with width at most k, and hence in GNF.

Now we prove the correctness of the reduction. Suppose QA(F 0 0 , ⌃ 0 , Q) holds, so any F 0 ◆ F 0 0 satisfying ⌃ 0 must satisfy Q. Now consider F ◆ F 0 that satisfies ⌃ and where all R + in D are transitive. We must show that F satisfies Q. First, observe that F satisfies ⌃ 0 since the k-guardedlytransitive axioms for R + are clearly satisfied for all k when R + is transitively closed. Now consider the extension of F to F 0 with additional facts G(a, b) for all a, b 2 elems(F 0 ). This must still satisfy ⌃ 0 : adding these guards means there are additional k-guardedly-transitive requirements on the elements from F 0 , but these requirements already hold since R + is transitively closed on all elements. Hence, by our initial assumption, F 0 must satisfy Q. Since Q does not mention G, the restriction of F 0 back to F still satisfies Q as well. Therefore, QA(F 0 , ⌃, Q) holds.

On the other hand, suppose for the sake of contradiction that QA(F 0 0 , ⌃ 0 , Q) does not hold, but QAtr(F 0 , ⌃, Q) does. Then there is some F 0 ◆ F 0 0 such that F 0 satisfies ⌃ 0 ^¬Q, and hence also satisfies ⌃ ^¬Q. Since ⌃ ^¬Q is in BaseGNF, Proposition 11 implies that we can take F 0 to be a set of facts that has an F 0 0 -rooted (k 1)-width base-guardedinterface tree decomposition. Let F 00 be the result of taking the transitive closure of the distinguished relations in F 0

. By Lemma 5, transitively closing like this can only add R + -facts about pairs of elements that are not base-guarded. Moreover, Lemma 7 ensures that adding R + -facts about these nonbase-guarded pairs of elements does not affect satisfaction of BaseCovGNF sentences, so F 00 must still satisfy ⌃ ^¬Q. Restricting F 00 to its -facts results in an F where every distinguished relation is transitively closed and where ⌃ ^¬Q is still satisfied, since ⌃ and Q do not mention relation G. But this contradicts the assumption that QAtr(F 0 , ⌃, Q) holds.

This concludes the proof of correctness. Finally, observe that the k-guardedly-transitive axioms can be written as FGTGDs (in fact, BaseFGTGDs): they are equivalent to the conjunction of FGTGDs of the form 8x y x 1 . . .

x l+1 ⇥ x = x 1 ^xl+1 = y R+ (x 1 , x 2 ) ^• • • ^R+ (x l , x l+1 ) ^S(x, y) ! R + (x, y) ⇤ for all S 2 B [ {G}, 1  l  k, and R + 2 D . Therefore, if ⌃ is in BaseCovFGTGD then ⌃ 0 is in FGTGD as claimed.
Theorem 4 easily follows from this. Proof of Theorem 4. Recall that we have fixed constraints ⌃ in BaseCovFGTGD and a base-covered UCQ Q. We must show PTIME data complexity of QAtr(F 0 , ⌃, Q) for any finite initial set of facts F 0 . Use Proposition 15 to construct ⌃ 0 from ⌃ (in constant time, since ⌃ is fixed) and

F 0 0 from F 0 (in time polynomial in |F 0 |). Since ⌃ is in BaseCovFGTGD, ⌃ 0
is in FGTGD. Therefore, the PTIME data complexity upper bound for QAtr with BaseCovFGTGDs follows from the PTIME data complexity upper bound for QA with FGTGDs [START_REF] Baget | [END_REF].

G Hardness results

Chase. In the proofs of this section and of subsequent sections, we will need the standard database construction of the chase [START_REF] Abiteboul | [END_REF] by TGDs: Definition 1. The chase applies to a set of facts F and to a set ⌃ of TGDs, and constructs a set of facts F 0 ◆ F, possibly infinite, which satisfies ⌃, in the following manner.

We first define a chase round as follows: for each TGD ⌧ : 8x '(x) ! 9ỹ (x, ỹ), for each homomorphism h from x to the elements of F such that the facts of '(h(x)) are in F, if h does not extend to a homomorphism from x [ ỹ such that the facts of (h(x), h(ỹ)) hold in F, then we call '(h(x)) a violation of ⌧ in F: we repair it by creating fresh elements (called existential witnesses) b for each variable of ỹ, and add to F the facts (h(x), b).

Applying a chase round means performing this process in parallel for all TGDs and violations, creating fresh existential witnesses for each TGD and violation. The chase of F by ⌃ is the (potentially infinite) set of facts obtained by repeated applications of chase rounds.

When we use the chase, we will often use the fact that the result satisfies ⌃, and that all existentially quantified variables when applying rules are instantiated by fresh existential witnesses (so no new facts are created on an element unless it occurs on a fact which is part of a violation).

G.1 Proof of Theorems 5 and 7

The hardness results for QAtc and QAlin mentioned in the body depend on the reductions described in Theorems 5 and 7. We start by proving Theorem 5, and we will adapt the proof afterwards to show Theorem 7.

Recall the result statement: Theorem 5. For any finite set of facts F 0 , DIDs ⌃, and UCQ Q on a signature , we can compute in PTIME a set of facts F 0 0 , BaseIDs ⌃ 0 , and a base-covered CQ Q 0 on a signature 0 (with a single distinguished relation), such that

QA(F 0 , ⌃, Q) iff QAtc(F 0 0 , ⌃ 0 , Q 0 ).
We start by creating a UCQ Q 0 , and then modify the proof to make Q 0 a CQ. Throughout the proof, whenever we talk of the DIDs in ⌃, we mean all dependencies of ⌃, including those where the head is a trivial disjunction with only one disjunct.

Definition of the reduction. Create the signature 0 from and ⌃ by: • adding a fresh binary base predicate E and taking the transitive closure E + of E as the one distinguished relation of 0 ; • replacing each predicate R in with a base predicate R 0 in 0 of arity arity(R) + 2;

• adding to 0 , for each DID of the form

⌧ : 8x R(x) ! _ 1in 9ỹ i R i (x, ỹi ),
a base predicate witness ⌧ (x, ỹ1 , e 1 , f 1 , . . . , ỹn , e n , f n ).

We create ⌃ 0 from ⌃ by replacing each

DID ⌧ : 8x R(x) ! W 1in 9ỹ i R i (x, ỹi ) by BaseIDs equivalent to: 8x e f R 0 (x, e, f ) ! 9 ỹ1 e 1 f 1 , . . . , ỹn e n f n witness ⌧ (x, ỹ1 , e 1 , f 1 , . . . , ỹn , e n , f n )î R 0 i (x, ỹi , e i , f i ) ^E+ (e i , f i )
Note that we have written the BaseIDs for a given ⌧ as a single TGD above with multiple conjuncts in the head, but we can easily rewrite them as multiple BaseIDs for ⌧ : the first one has the same body and the witness ⌧ -fact as head atom, and the others have the witness ⌧ -fact as body atom and each one of the other facts as head atom.

The intuition for the proof is that a fact R(c) over the original schema will correspond to facts R 0 (c, e, f ) in the new schema with fresh elements e and f . The fresh elements will always be connected by an E-path (as required by the E + fact), which will be imposed (via failure of the query) to have length 1 or 2. Facts of this type with a path of length 1 will be called genuine facts, which intuitively hold, and those with a path of length 2 will be called pseudo-facts and will be ignored by the query.

This mechanism allows us to eliminate disjunction from DIDs as follows: we require that, when the body atom holds, there are witness facts R 0 i (c, di , e i , f i ) for all of the disjuncts. However, we will use the query to require that, when the match of the body atom is a genuine fact, not all disjuncts can be pseudo-facts, so one of them must be a genuine fact; the others can be made pseudo-facts. Note that ⌃ 0 still requires matches for all of the disjuncts even when the body is matched to a pseudo-fact; however, the query will only require that one of the head atoms is matched to a genuine fact when the body is itself matched to a genuine fact. To this end, we will call the sequence c, d1 , e 1 , f 1 , . . . , dn , e n , f n will be called a witness vector for R(c) and ⌧ , and we capture such witness vectors in the predicate witness ⌧ . The UCQ Q 0 contains the following disjuncts: • Q-generated disjuncts: One disjunct for each disjunct of the original UCQ Q, where each atom R(x) is replaced by the conjunction R 0 (x, e, f ) ^E(e, f ), where e and f are fresh. That is, we have a witness for Q consisting of genuine facts.

• E-path length restriction disjuncts: For each predicate R in , we have a disjunct that succeeds if the E-path for an R 0 -fact has length 3, i.e., R 0 (x, e, f) ^E(e, y 1 ) Ê(y 1 , y 2 ) ^E(y 2 , y 3 ). Intuitively, for every R 0 -fact, the E + -fact on its two last elements must make it either a genuine fact or a pseudo-fact.

• DID satisfaction disjuncts: For every DID ⌧ :

8x R(x) ! W i 9ỹ i R i (x, ỹi ) in ⌃, we have a disjunct Q ⌧ :R 0 (x, e, f ) ^E(e, f ) ^witness ⌧ (x, ỹ1 , e 1 , f 1 , . . . , ỹn , e n , f n ) ^1in R 0 i (x, ỹi , e i , f i ) ^(E(e i , w i ) ^E(w i , f i ))
Informally, the failure of Q ⌧ enforces that we cannot have the body of ⌧ holding as a genuine fact and each of the components of the witness vector realized by a pseudo-fact.

Observe that all of these disjuncts are trivially base-covered (since they do not use E +

). We now explain how to rewrite the facts of an initial fact set F 0 on to a fact set F 0 0 on 0 . Create F 0 0 by replacing each fact

F = R(ã) of F 0 by the facts R 0 (ã, b F , b 0 F ), and E(b F , b 0 F )
, where b F and b 0 F are fresh, so that they are genuine facts.

Correctness proof for the reduction. We now show that the claimed equivalence holds:

QA(F 0 , ⌃, Q) holds iff QAtc(F 0 0 , ⌃ 0 , Q 0 ) holds. First, let F ◆ F 0 satisfy ⌃ and violate Q. We must con- struct F 0 that satisfies ⌃ 0 and violates Q 0 (when interpreting E +
as the transitive closure of E). We construct F 0 using the following steps: • Modify F in the same way that we used to build F 0 0 from F 0 (i.e., expand each fact with two fresh elements with an E-edge between them), yielding F 1 ;

• We now need to ensure that witnesses exist as required by ⌃ 0

, which we will create as pseudo-facts. For every DID ⌧ of ⌃ and fact F = R(c) of F that matches the body of ⌧ , as F satisfies ⌃, there is at least one i 0 such that some fact R i0 (c, di0 ) witnesses that ⌧ is not violated in F. Call I the set of such indices for which a witness exists in F. We then know by construction that, for all i 2 I, the set of facts

F 1 contains F i • • = R 0 i (c, di , e i , f i ) and F 0 i • • = E(e i , f i )
for some e i and f i . For every i 2 {1, . . . , n}\I, create a fresh di , e i , f i , w i and add a fact R 0 i (c, di , e i , f i ) along with the facts E(e i , w i ) and E(w i , g i ) indicating that this is a pseudo-fact. We also add a fact witness ⌧ (c, d1 , e 1 , f 1 . . . dn , e n , f n ) containing the witness vector consisting of the elements of the F i above (those that we created, for i 2 {1, . . . , n}\I, and those that already existed, for i 2 I). We call F 2 the result of performing this process simultaneously in all places where it is applicable. Observe that, in F 2 , we have ensured that no rule of ⌃ 0 has a violation whose body matches a genuine fact.

• The above process creates new pseudo-facts, and we also have to satisfy the rules of ⌃ 0 for these. We create F 3 from F 2 by simply chasing with ⌃ 0 wherever applicable (see Definition 1), always creating fresh elements; whenever we need a witness for some E + requirement, we always create an E-path of length 2 with a fresh element in the middle, that is, we always create pseudofacts.

Let

F 0 • • = F 3 . It is clear that F 0 ◆ F 0 0
and that E + is indeed the transitive closure of E, and it is immediate by definition of the chase that F 0 satisfies ⌃ 0 , so we must check that F 0 violates Q 0 , which we do by considering each kind of disjunct.

For the E-path length restriction disjuncts observe that we only create paths of length 1 or 2 of E (of length 1 when creating F 1 , and of length 2 when creating F 2 and F 3 ). We always create these paths on fresh elements, so these paths of length 1 and 2 are never connected; hence, there is no E-path of length 3 at all in F 0 . For the DID satisfaction disjuncts, assume by contradiction that there is a match for a disjunct

Q ⌧ of Q 0 in F 0 . Fix c, e, f such that R 0 (c, e, f ) ^E(e, f ) holds, a fact witness ⌧ (c, d1 , e 1 , f 1 . . . dn , e n , f n ), and pseudo-facts R 0 i (c, di , e i , f i ) with e i , f
i connected by paths of length 2. The genuine fact R 0 (c, e, f ) could not have been generated within either of the second or third steps in the creation of F 0 above, since all the R 0 -facts generated there have paths only of length 2 between the last two components (that is, they are pseudo-facts). Thus R 0 (c, e, f ) must have been generated in the first step, coming from fact R(c) in F. But then, as F satisfies ⌧ , there must be i 0  n such that F contains R i0 (c, di0 ) for some di0 , and thus

F 1 must con- tain R 0 i0 (c, di0 , e i0 , f i0
) and E(e i0 , f i0 ) for some e i0 and f i0 . Further, the witness ⌧ -fact must have been created in the second step above, as the other witness ⌧ -facts are created during the third step, where they only cover pseudo-facts rather than genuine facts. Hence, in creating the witness vector corresponding to R(c, e, f ) in the second step, we would not have generated a path of length 2 for e i0 , f i0 (as we would have had i 0 2 I), a contradiction.

Finally, for the Q-generated disjuncts, observe that any match of them must be on facts of F 0 created for facts of F (as they are annotated by E-paths of length 1), so we can conclude because F violates Q.

Hence, F 0 satisfies ⌃ 0 and violates Q 0 , which concludes the first direction.

In the other direction, let F 0 ◆ F 0 0 be a counterexample to QAtc(F 0 0 , ⌃ 0 , Q 0 ). Consider the set of R 0 -facts from F 0 such that R 0 2 0 corresponds to some R 2 and the elements in the last two positions of this R 0 -fact are connected by an E-fact, i.e., the genuine facts. Construct a set of facts F on by projecting away the last two positions from these R 0 -facts, and discarding all of the other facts.

It is clear by construction of F 0 0 that F ◆ F 0 and that E + is indeed the transitive closure of E in F. Further, as

F 0 violates Q 0 , it is clear that F violates Q, as any match of a disjunct of Q on F implies a match of the corresponding Q-generated disjunct Q 0 in F 0 . So it suffices to show that F satisfies ⌃.
Assume by contradiction that some DID ⌧ of ⌃ is violated on a fact F = R(x) of F (that is F matches the body of ⌧ ). Let F 0 = R 0 (c, e, f ) be the fact in F 0 from which we created F ; we know that the last two elements of F 0 are connected by an E-fact. Since F 0 satisfies ⌃ 0 , we know that there are d1 , e , we know that for each i, there is some E-path connecting e i and f i . By the E-path length-restriction disjuncts and DID satisfaction disjuncts, it must be the case that there is an E-path of length at most 2 between each e i and f i , and for some j there cannot be a path of length 2 between e j and f j (otherwise, F 0 would satisfy the corresponding DID satisfaction disjunct in Q 0

), so then the path must have length 1. But this means that F 0 contains R 0 j (c, dj , e j , f j ) and E(e j , f j ), so R j (c, dj ) is a fact in F witnessing the satisfaction of DID ⌧ , a contradiction. Hence, F satisfies ⌃, which concludes the proof.

From UCQ to CQ. Last, we explain how to replace the UCQ Q 0 by a CQ. We do this by a general process that we will reuse in several upcoming proofs: intuitively, we increase the arity to annotate facts with an additional Boolean value carried over in dependencies and add an Or-relation to combine such values. Define Q 00 from Q 0 as follows: • Add to the atoms of each disjunct of Q 0

(except Eatoms) one common variable which is shared between all atoms and left free: we call each resulting CQ Q i (w i ), where w i is the new variable. • Define the Boolean CQ Q 00 as the following (existentially closed), where m is the number of disjuncts of Q 0 : Or(w 1 , w 2 , w 0 1 ) ^Or(w 0

1 , w 3 , w 0 2 ) ^• • • ^Or(w 0 m 2 , w m , w 0 m 1 ) ^True(w 0 m 1 ) ^1im Q i (w i )
Note that Q 00 is trivially covered. Define the set of facts F 00 0 from F 0 0 by: • Adding the facts of F Or ; • Putting t as the last element of all other facts except Efacts;

• Adding vacuous matches: for each Q i (w i ), we add a set of facts that satisfy Q i (w i ), with f as the common last element of all facts, but the domains being otherwise disjoint. Intuitively, the purpose of the vacuous matches is to ensure that the Q i (w i ) always have a match but with w i set to false, and otherwise they have no purpose and they simply do not interact with the other facts. We accordingly call an element vacuous in a set of facts if it occurs in no fact with t as the last element, and call a fact vacuous if it is an E-or E + -fact on vacuous elements, or it is a fact for another relation than E but its last element is not t.

We will now show the following equivalence: QAtc(F 0 0 , ⌃ 0 , Q 0 ) iff QAtc(F 00 0 , ⌃ 00 , Q 00 ), which concludes the proof.

In one direction, we assume we have a counterexample F 0 to QAtc(F 0 0 , ⌃ 0 , Q 0 ). We construct F 00 from F 0 by extending it according to the process above (to define F 00 0 from F 0 0 ), and chasing by ⌃ 00 on all facts from the vacuous matches (see Definition 1), with f being propagated as the last element, so the resulting elements and facts are all vacuous. We claim that F 00 witnesses the failure of QAtc(F 00 0 , ⌃ 00 , Q 00 ). It is clear that F 00 is a superset of F 00 0 and that E + is indeed interpreted as the transitive closure of E. We argue that ⌃ 00 is satisfied by F 00 , by looking whether the required witness facts exist for each type of fact. Vacuous facts have the required witnesses because we chased them in constructing F 00

. No constraints of ⌃ 00 hold about the facts from F Or . Finally, for the facts of F 00 created from facts of F 0 , they have the required witnesses because ⌃ 0 was satisfied by F 0 and the last position of such a fact is always t so the last variable was correctly exported.

We now explain why F 00 violates Q 00 . Assuming by contradiction that F 00 satisfies Q 00 , by definition of the Orand True-facts that F 00 contains by construction, it must be the case that F 00 satisfies Q i (t) for some Q i . But it is then clear that F 0 satisfies the corresponding disjunct of Q 0 , as this match cannot involve any vacuous facts. This proves one direction.

For the other direction, we assume we have a counterexample F 00

for QAtc(F 00 0 , ⌃ 00 , Q 00 ). We construct F 0 from F 00 by keeping only the facts in the base signature with last element t and keeping precisely the E-and E + -facts that are connected to them. It is clear that, as F 00 ◆ F 00 0 , we have F 0 ◆ F 0 0 . To see that F 0 satisfies ⌃ 0 , assume by contradiction that F 0 witnesses a violation of an ID ⌧ 0 of ⌃ 0 in F 0 , and let F 00 be the corresponding fact in F 00 . By definition of ⌃ 00 , there is a corresponding ID ⌧ 00 in ⌃ 00 that asserts the existence of a fact F 00 2 . So the only way F 0 can violate ⌧ 0 is that F 00 2 is an E-fact or that the last element of F 00 2 is not t, but as the last element of F 00 is t, this is impossible. Hence, we have a contradiction, and F 0 satisfies ⌃ 0 . The only thing left to show is that F 0 violates Q 0 . Assuming to the contrary that F 0 satisfies some disjunct of Q 0 , we know that, considering the corresponding Q i (w i ), F 00 satisfies Q i (t). Now, from the facts in F Or ✓ F 00 , and from the vacuous matches and their connected E -and E + -facts, we know that we can construct a match of the entire CQ Q 00 in F 00

, a contradiction as F 00 violates Q 0 . This concludes the correctness proof, and concludes the proof of Theorem 5.

We now prove Theorem 7, which states: Theorem 7. For any finite set of facts F 0 , DIDs ⌃, and UCQ Q on a signature , we can compute in PTIME a set of facts F 0 0 , BaseIDs ⌃ 0 , and CQ Q 0 on a signature 0 (with a single distinguished relation), such that QA(F 0 , ⌃, Q) iff QAlin(F 0 0 , ⌃ 0 , Q 0 ).

The entire proof is shown by adapting the proof of Theorem 5. We start by showing the claim with a UCQ. Intuitively, instead of using E + to emulate a disjunction on the length of the path to encode genuine facts and pseudo facts, we will use the order relation to emulate disjunction on the same elements: e < f will indicate a genuine fact, whereas f < e will indicate a pseudo-fact, and e = f will be prohibited by the query.

Definition of the reduction. We define 0 as in the proof of Theorem 5, except that we do not add the predicates E and E +

, but add a predicate < as a distinguished relation instead. We also define ⌃ 0 as before except that we drop all mention of E + . The UCQ Q 0 contains the following disjuncts (existentially closed):

• Order restriction disjuncts: For each R 2 , we have a disjunct R 0 (x, e, e) to enforce disjunction between genuine facts and pseudo-facts. • Q-generated disjuncts: Each disjunct of the original UCQ Q, where each atom R(x) is replaced by the conjunction R 0 (x, z, z 0 ) ^z < z 0

, where z and z 0 are fresh. That is, we have a witness for Q consisting of genuine facts.

• DID satisfaction disjuncts: For every DID ⌧ :

8x R(x) ! W i 9ỹ i R i (x, ỹi ) in ⌃, we have a disjunct Q ⌧ : R 0 (x, e, f ) ^e < f ^witness ⌧ (x, ỹ1 , e 1 , f 1 . . . ỹn , e n , f n ) ^1in R 0 i (x, ỹi , e i , f i ) ^fi < e i
Intuitively, Q ⌧ is satisfied if the body of ⌧ is matched to a genuine fact but each of the components of the witness vector is matched to a pseudo-fact. Observe that all CQs of the resulting UCQ are base-covered, as required.

The process to define F 0 0 from F 0 is defined like in the proof of Theorem 5 except that we remove the E-facts and replace them by b F < b 0 F .

Correctness proof for the reduction. The proof that QA(F 0 , ⌃, Q) holds iff QAlin(F 0 0 , ⌃ 0 , Q 0 ) holds is similar to the proof for Theorem 5, so we sketch the proof and highlight the main differences.

For one direction, let F ◆ F 0 satisfy ⌃ and violate Q. We construct F 0 from F as follows: • Construct F 1 from F as we constructed F 0 0 from F 0 above.

• The construction of F 2 and F 3 is as before, except that we create a <-fact to indicate a pseudo-fact.

• The new step is that F 0 is constructed from F 3 by completing < to be a total order. To do so, however, we must ensure that our definition of < in F 3 does not contain any cycles. This is easy to see, however: we only imposed an order relation between disjoint pairs of elements. Hence, it is clear that < cannot contain any loop, so we can simply complete this partial order to a total order using the order extension principle [Szpilrajn, 1930].

As before it is clear that F 0 ◆ F 0 0 and that F 0 satisfies ⌃ 0

, and we have made sure that < is a total order. To see why Q 0 is not satisfied in F 0 , we proceed exactly as before for the DID satisfaction disjuncts and Q-generated disjuncts, but replacing "having an E-fact between e and f " by "having e < f", and replacing "having an E-path of length 2 between e and f " by "having e > f", and likewise for e i and f i . By construction, we never have e = f or e i = f i in any fact within F 0 , so we also do not match the order-restriction disjuncts in Q 0 . For the other direction, suppose we have some counterexample F 0 to QAtc(F 0 0 , ⌃ 0 , Q 0 ). We construct F from F 0 by keeping all facts whose last two elements e and f are such that e < f. The result still clearly satisfies F ◆ F 0 , and the proof of why it violates Q is unchanged. To show that F satisfies ⌃, we adapt the argument of the proof of Theorem 5, but instead of relying on the E-path length disjuncts we rely on totality of the order and the order-restriction disjuncts. Totality of the order ensures that for fact F ⌧ , and for all i, we have either e i < f i , e i = f i and f i < e i . But the orderrestriction disjuncts are violated, so it must be either e i < f i or f i < e i , and the DID satisfaction disjuncts of Q are violated, so we must have e i < f i for some i. Hence, we can argue as before that the satisfaction of ⌃ 0 by F 0 ensures that ⌃ is satisfied in F.

From UCQ to CQ. The proof from UCQ to CQ works exactly like before, except that we do not increase the arity of < (recall that we did not increase the arity of E + and E), and we use QAlin instead of QAtc. When showing that we can construct a counterexample to F 00 to QAlin(F 00 0 , ⌃ 00 , Q 00 ) from a counterexample to QAlin(F 0 0 , ⌃ 0 , Q 0 ), we make < a total order in F 00 using again the order extension principle (the order on vacuous matches, and on the domain elements of F Or , is arbitrary). Observe that the resulting CQ is clearly basecovered, as all disjuncts of the UCQ Q 0 were base-covered.

G.2 Proof of Propositions 2 and 4

We now give data complexity lower bounds that show CoNPhardness even in the absence of constraints. We first prove Proposition 2: Proposition 2. There is a base-covered CQ Q such that the data complexity of QAtc(F 0 , ;, Q) is CoNP-hard.

Proof. We first prove the result for a UCQ Q, and then for a CQ Q 0 .

Definition of the reduction. We define the signature as containing:

• one binary predicate E and its transitive closure E + (again playing a similar role as in the proof Theorem 5); • one binary relation G to code the edges of a graph which will be provided as input to the reduction; • one 7-ary relation V to code vertices and their color. The idea is that one position is for the vertex and then for each of the 3 colors we will have two positions that will encode whether or not the vertex has that color. If the positions associated with a color C are connected by an E-edge, this will indicate coloring the vertex with color C, while if they are connecting by a path of length 2 this will indicate not being colored with color C.

We then define the UCQ Q to contain the following disjuncts (existentially closed):

• E-path length restriction disjuncts: For each predicate R in , we enforce that the E-path for the R 0 -fact has length 3: R 0 (x, e, f) ^E(e, y 1 ) ^E(y 1 , y 2 ) Ê(y 2 , y 3 ). • Adjacency disjuncts: For i 2 {1, 2, 3}, the disjunct Q i that succeeds if two adjacent vertices were assigned the same color:

V (x, e 1 , f 1 , e 2 , f 2 , e 3 , f 3 ) ^G(x, x 0 ) ^V (x 0 , e 0 1 , f 0 1 , e 0 2 , f 0 2 , e 0 3 , f 0 3 ) ^E(e i , f i ) ^E(e 0 i , f 0 i ) • Coloring disjunct: A disjunct that succeeds if a vertex
was not assigned any color:

V (x, e 1 , f 1 , e 2 , f 2 , e 3 , f 3 ) Vi2{1,2,3} E(e i , w i ) ^E(w i , f i )
Given a directed graph G, we code it in PTIME as the instance F 0 defined by having:

• One fact G(x, y) for each edge (x, y) in G

• The facts V (x, e

x,1 , f x,1 , e x,2 , f x,2 , e x,3 , f x,3 ) and E + (e

x,i , f x,i ) for i 2 {1, 2, 3} for each vertex x in G(x, y), where all the e

x,i and f x,i are fresh.

Correctness proof for the reduction. We now show that G is 3-colorable iff QAtc(F 0 , ;, Q) is false, completing the reduction.

First, consider a 3-coloring of G. Construct F ◆ F 0 as follows. For each vertex x of G (with corresponding V -fact V (x, e

x,1 , f x,1 , e x,2 , f x,2 , e x,3 , f x,3 ) as defined above) create the facts E(e

x,i , f x,i ) where i is the color assigned to x, and the facts E(e x,j , w x,j ) and E(w x,j , f x,j ) for the other colors j 2 {1, 2, 3}\{i} (with the two w

x,j being fresh). It is clear that F thus defined is such that F ◆ F 0 , and that E + is the transitive closure of E in F. The E-path length restriction disjuncts of Q do not match in F (note that we only create Epaths whose endpoints are pairwise distinct), and the coloring disjunct does not match either. Finally, the fact that we have a 3-coloring ensures that the adjacency disjuncts do not match either. Hence, we have a set of facts violating Q.

For the other direction, consider some F ◆ F 0 that violates Q. Since F violates the first and last disjunct of Q and E + is the transitive closure of E, any vertex x of G (with corresponding V -fact V (x, e

x,1 , f x,1 , e x,2 , f x,2 , e x,3 , f x,3 ) defined above) there must be an E-path of length 1 or 2 from e

x,i to f x,i for all i 2 {1, 2, 3}. Further, as F violates the last disjunct of Q, at least one of these paths must have length 1. Define a coloring of G by giving each vertex x a color i such that E(e x,i , f x,i ) holds in the V -fact for x. This indeed defines a 3-coloring, as any violation of the 3-coloring witnessed by two adjacent vertices of color i would imply a match of Q i in F.

From UCQ to CQ. We replace the UCQ Q by a CQ Q 0 in the same manner as in the proof of Theorem 5: we increase the arity of all predicates and add the relations of Or , add to F 0 the facts of F Or and the vacuous matches, and rewrite the query as in the proof of Theorem 5. We can then adapt the argument of that proof to show that the resulting QAtc problem with the CQ is equivalent to the previously defined problem with a UCQ.

We then modify the proof to show Proposition 4:

Proposition 4. There is a base-covered CQ Q such that the data complexity of QAlin(F, ;, Q) is CoNP-hard.

Proof. We define as in the previous proof but with an order relation < and without E, E + . We define Q as in the proof of Proposition 2 but without its first disjunct, and replacing in the other disjuncts E(e i , f i ) by e i < f i , and

E(e i , w i ) Ê(w i , f i ) by f i < e i .
Unlike in the proof of Theorem 7, we need not worry about equalities (and we need not add order restriction disjuncts), as all the elements of relevant V -facts are created already in F 0 , where they are created as distinct elements. We define F 0 in the same fashion as in the proof of Proposition 2 but without the E + -facts. We prove the same equivalence as in that proof but for QAlin. We do it by replacing E-paths of length 1 from an e-element to an f -element by e < f, and E-paths of length 2 by f < e.

We replace the UCQ by a CQ exactly as in the other proof. As in the proof of Theorem 7, the order on the vacuous matches is arbitrary.

H Undecidability results related to transitivity (from Section 5)

We first prove the second result as it is simpler to understand. Theorem 9. There is an arity-two signature = B t D with a single distinguished predicate S + in D , a set ⌃ of DIDs on , a CQ Q on B , such that the following problem is undecidable: given a finite set of facts F 0 , decide QAtr(F 0 , ⌃, Q). Proof. As in Proposition 4, we first prove the result with a UCQ and then modify the proof to use a CQ.

An infinite tiling problem is specified by a set of colors C = C 1 , . . . , C k , a set of forbidden horizontal patterns H ✓ C 2 and a set of forbidden vertical patterns V ✓ C 2

. It asks, given a sequence c 0 , . . . , c n of colors of C, whether there exists a function f : N 2 ! C such that f ((0, i)) = c i for all 0  i  n, and for all i, j 2 N, we have (f (i, j), f(i + 1, j)) / 2 H and (f (i, j), f(i, j + 1)) / 2 V.

It is well-known that we can take C, V, H such that the corresponding tiling problem is undecidable; we fix such a problem.

Definition of the reduction. We define a binary relation S 0 (for "successor"), a transitive relation S + , one binary relation K i for each color C i , and one unary relation K 0 i for each color C i .

We write the following DIDs ⌃ (note that they are not baseguarded), dropping universal quantification for brevity:

S 0 (x, y) ! 9z S 0 (y, z) S 0 (x, y) ! S + (x, y) S + (x, y) ! _ i K i (x, y) S + (x, y) ! _ i K i (y, x) S + (x, y) ! _ i K 0 i (x)
Intuitively, K 0 i (x) stands for K i (x, x), but we need a different predicate because variable reuse is not allowed in inclusion dependencies.

The UCQ Q is a disjunction of the following disjuncts (existentially closed):

• For each forbidden horizontal pair (C i , C j ) 2 H, with 1  i, j  k, the disjuncts:

K i (x, y) ^S0 (y, y 0 ) ^Kj (x, y 0 ) K 0 i (y) ^S0 (y, y 0 ) ^Kj (y, y 0 ) K i (y 0 , y) ^S0 (y, y 0 ) ^K0 j (y 0 ) • For each forbidden vertical pair (C i , C j ) 2 V, the anal- ogous disjuncts: K i (x, y) ^S0 (x, x 0 ) ^Kj (x 0 , y) K 0 i (x) ^S0 (x, x 0 ) ^Kj (x 0 , x) K i (x, x 0 ) ^S0 (x, x 0 ) ^K0 j (x 0 )
Given an initial instance of the tiling problem c 0 , . . . , c n , we encode it in the initial set of facts F 0 :

• S 0 (a i , a i+1 ) for 0  i < n; • for 0 < i  n, the fact K j (a 0 , a i ) such that C j is the color of initial element c i ; • the fact K 0 j (a 0 ) such that C j is the color of c 0 .

Correctness proof for the reduction. We claim that the tiling problem has a solution iff there is a (generally infinite) superset of F 0 that satisfies ⌃ and violates Q and where S + is transitive. From this we conclude the reduction and deduce the undecidability of QAtr as stated.

For the forward direction, from a solution f to the tiling problem for input c, we construct the counterexample F ◆ F 0 as follows. We first create an infinite chain S 0 (a 0 , a 1 ), . . . , S 0 (a m , a m+1 ), . . . to complete the initial chain of S 0 -facts in F 0 , and fix S + to be the transitive closure of this S 0 -chain (so it is indeed transitive). For all i, j 2 N such that i 6 = j, we create the fact K l (a i , a j ) where l = f (i, j). For all i 2 N, we create the fact K 0 l (a i ) where l = f (i, i). This clearly satisfies the constraints in ⌃, and does not satisfy the query because f is a tiling.

For the backward direction, consider a F ◆ F 0 that satisfies ⌃ and violates Q. Starting at the chain of S 0 -facts of F 0 , we can deduce, using the constraints, the existence of an infinite chain a 0 , . . . , a n , . . . of S 0 -facts (whose elements may be distinct or not, this does not matter). Define a tiling f matching the initial tiling problem instance as follows. For all i < j in N, as there is a path of S 0 -facts from a i to a j , we infer that S + (a i , a j ) holds, so that K l (a i , a j ) holds for some 1  l  k; pick one such fact, taking the fact of F 0 if i = 0 and j  n, and fix f (i, j) • • = l. For i > j we can likewise see that S + (a j , a i ) holds whence K l (a i , a j ) holds for some l, and we continue as before. For i 2 N, as S 0 (a i , a i+1 ) holds, we know that K l (a i ) holds for some 1  l  k (again we take the fact of F 0 if i = 0), and fix accordingly f (i, i) • • = l. The resulting f clearly satisfies the initial tiling problem instance c 0 , . . . , c n , and it is clearly a solution to the tiling problem, as any forbidden pattern in f would witness a match of a CQ of Q in F. This shows that the reduction is correct, and concludes the proof with the UCQ Q.

From UCQ to CQ. We now adapt the proof to use a CQ, similarly to the proof of Theorem 5: we use the signature 0 Or constructed by extending S 0 (and only S 0 ) to have a third position, and adding the relations of Or (see the proof of Theorem 5). We modify ⌃ by changing the first dependency to propagate also the third element of the S 0 -atoms, i.e., 8x y b S 0 (x, y, b) ! 9z S 0 (y, z, b), and replace the second dependency similarly by 8x y b S 0 (x, y, b) ! S + (x, y). We construct the CQ Q 0 from the UCQ Q by adding one variable b to each S 0 -fact of each disjunct, and connecting these disjuncts on their free variables with Or-facts and adding a True-fact as in the proof of Theorem 5.

We then define the initial set of facts F 0 0 to include the facts of F Or , the facts of F 0 where each S 0 is extended by adding t as its third element, and vacuous matches for each Q i (defined as in the proof of Theorem 5, with the element f at the third position of each S 0 -fact, all the vacuous matches having pairwise disjoint domains except for f).

To show the forward direction, we construct F from F 0 as before but with t at the third position of all created S 0 facts, plus a completion of the vacuous matches obtained by chasing (see Definition 1). Like in the proof of Theorem 5, any match of the CQ Q 0 must imply a match of one of the disjuncts of the UCQ Q, and as this match must be on an S 0 -fact with t as third position, it cannot involve a vacuous match, so we conclude as before.

Conversely, for the backward direction, we define the tiling analogously to what we did before, and we observe that any violation of the tiling property would imply a match of one disjunct of the UCQ Q, which we can extend thanks to the vacuous matches to a match of Q 0

. This concludes the proof.

We now prove the first statement, drawing inspiration from the previous proof, but using the transitive closure to emulate disjunction as in Theorem 5. Recall the statement:

Theorem 8. There is a signature = B t D with a single distinguished predicate S + in D , a set ⌃ of IDs on , and a CQ Q on B , such that the following problem is undecidable: given a finite set of facts F 0 , decide QAtc(F 0 , ⌃, Q). Proof. We reuse the notations for tiling problems from the previous proof. We first prove the result with two distinguished relations S + and C + and with a UCQ, and then explain how the proof is modified to use only a single transitive relation S +

, and finally explain how to adapt the proof to use a CQ rather than a UCQ.

Definition of the reduction. We define a binary relation S (for "successor") of which S + is interpreted as the transitive closure, one binary relation S 0

, one 3-ary relation G (for "grid"), one binary relation G 0

(standing for the diagonal cells of the grid), one binary relation T (a terminal for gadgets that we will define to indicate colors) and one binary relation C of which C + is interpreted as the transitive closure. The distinction between S and S 0 is not important for now but will be important when we adapt the proof later to use a single distinguished relation.

We write the following inclusion dependencies ⌃ (with universal quantification dropped for brevity):

S 0 (x, y) ! 9z S 0 (y, z) S 0 (x, y) ! S(x, y) S + (x, y) ! 9z G(x, y, z) S + (y, x) ! 9z G(x, y, z) S + (x, y) ! 9z G 0 (x, z) G(x, y, z) ! 9w T (z, w) G 0 (x, z) ! 9w T (z, w) T (z, w) ! C + (z, w)
In preparation for defining the query Q, we define Q i (z) for all i > 0 to match the left endpoint of T -facts covered by a C-path of length i (intuitively coding color i):

9z 1 . . . z i w C(z, z 1 )^C(z 1 , z 2 )^. . . , C(z i 1 , z i )^T (z, z i ),
The query Q is a disjunction of the following disjuncts (existentially closed):

• C-path sanity disjuncts: One disjunct written as follows,

where k is the number of colors

G(x, y, z) ^S0 (x, w) ^T (z, z) ^C(z, z 1 ) ^C(z 1 , z 2 ) ^• • • ^C(z k 1 , z k ) ^C+ (z k , z 0 )
and one disjunct defined similarly but with G(x, y, z) replaced by G 0 (x, z). Intuitively, these disjuncts impose that C-paths that cover T -facts must code colors between 1 and k, and the distinction between G and G 0 is for reasons similar to the distinction between the K i and K 0 i in the proof of Theorem 9. • Horizontal adjacency disjuncts: For each forbidden hor-

izontal pair (C i , C j ) 2 H, with 1  i, j  k, the dis- juncts: G(x, y, z) ^G(x, y 0 , z 0 ) ^Qi (z) ^Qj (z 0 ) ^S0 (y, y 0 ) G 0 (y, z) ^G(y, y 0 , z 0 ) ^Qi (z) ^Qj (z 0 ) ^S0 (y, y 0 ) G(y 0 , y, z) ^G0 (y 0 , z 0 ) ^Qi (z) ^Qj (z 0 ) ^S0 (y, y 0 ) • Vertical adjacency disjuncts: For each (C i , C j ) 2 V
, the same queries but replacing atoms S 0 (y, y 0 ) by S 0 (x, x 0 ) and the two first atoms of the last two subqueries by: -G 0 (x, z) ^G(x, x 0 , z 0 ) -G(x, x 0 , z) ^G0 (x 0 , z 0 )

Given an initial instance of the tiling problem c 0 , . . . , c n , we encode it in the initial set of facts F 0 :

• S 0 (a i , a i+1 ) for 0  i < n; • G(a 0 , a i , b 0,i ) for 0 < i  n; • G 0 (a 0 , b 0,0 )
• for all 0  i  n, letting j be such that c i is the j-th color C j , we create the length-j gadget on b 0,i : we create a path C(b 0,i , d 1 0

,i ), C(d 1 0,i , d 2 0,i ), . . . C(d j 1 0,i , d j 0,i ),
and the fact T (b 0,i , d j 0,i );

Correctness proof for the reduction. We claim that the tiling problem has a solution iff there is a (generally infinite) superset of F 0 that satisfies ⌃ and violates Q, where the S + and C + predicates are interpreted as the transitive closure of S and C, from which we conclude the reduction and deduce the undecidability of QAtc as stated.

For the forward direction, from a solution f to the tiling problem for input c, we construct F ◆ F 0 as follows. We first create an infinite chain S 0 (a 0 , a 1 ), . . . , S 0 (a m , a m+1 ), . . . to complete the initial chain of S 0 -facts in F 0 , we create the implied S-facts, and make S + the transitive closure. We then create one fact G(a i , a j , b i,j ) for all i 6 = j in N and one fact G 0 (a i , b i,i ) for all i 2 N. Last, for all i, j 2 N, letting l • • = f (i, j), we create the length-l gadget on b i,j with fresh elements.

It is clear that F contains the facts of F 0 . It is easy to verify that it satisfies ⌃. To see that we do not satisfy the query, observe that:

• The C-path sanity disjuncts have no match because all C-paths created have length  k and are on disjoint sets of elements; • For the horizontal adjacency disjuncts, it is clear that, in any match, z must be of the form b i,j and z 0 of the form b i,j+1 ; the reason for the three different forms is that the case where i = j and i 6 = j are managed differently. Then, as f respects H, we know that the Q i and Q j subqueries cannot be satisfied, because for any l 2 N and i 0 , j 0 2 N, we have Q l (b i 0

,j 0 ) iff f (i 0 , j 0 ) = l by construction;

• The reasoning for the vertical adjacency disjuncts is analogous. Hence, F ◆ F 0 , satisfies ⌃, and violates Q, which concludes the proof of the forward direction of the implication.

For the backward direction, consider a F ◆ F 0 that satisfies ⌃ and violates Q. Starting at the chain of S 0 -facts of F 0 , we can see that there is an infinite chain a 0 , . . . , a n , . . . of S 0

-facts (whose elements may be distinct or not, this does not matter), and hence we infer the existence of the corresponding S-facts. We can also infer the existence of elements b i,j for all i, j 2 N (again, these elements may be distinct or not) such that G 0 (a i , b i,i ) holds and G(a i , a j , b i,j ) holds if i 6 = j. From this we conclude that there is a fact T (b i,j , c i,j ) for all i, j 2 N, with a C-path from b i,j to c i,j . As the C-path sanity disjuncts are violated, there cannot be such a C-path of length k, so we can define a function f from N⇥N to C by setting f (i, j) to be c l where l is the length of one such path, for all i, j 2 N; this can be performed in a way that matches F 0 (by choosing the path that appears in F 0 if there is one). Now, assume by contradiction that f is not a valid tiling. If there are i, j 2 N such that (f (i, j), f(i, j + 1)) 2 H, then consider the match x • • = a i , y • • = a j , y 0 • • = a j+1 , z • • = b i,j , and z 0 • • = b i,j+1 . If i 6 = j and i 6 = j + 1, we know that G(a i , a j , b i,j ) and G(a i , a j+1 , b i,j+1 ) hold, and taking the witnessing paths used to define f (i, j) and f (i, j + 1), we obtain matches of Q f (i,j) (b i,j ) and Q f (i,j+1) (b i,j+1 ), so that we obtain a match of one of the disjuncts of Q (one of the first horizontal adjacency disjuncts), a contradiction. The cases where i = j and where i = j + 1 are similar and correspond to the second and third kinds of horizontal adjacency disjuncts. The case of V is handled similarly with the vertical adjacency disjuncts. Hence, f is a valid tiling, which concludes the proof of the backward direction of the implication, shows the equivalence, and concludes the reduction and the undecidability proof.

Adapting to a single distinguished relation. To prove the result with a single distinguished relation S +

, simply replace all occurrences of C and C + in the query and constraints by S and S + . The rest of the construction is unchanged. The proof of the backwards direction is unchanged, using S in place of C; what must be changed is the proof of the forward direction.

Let f be the solution to the tiling problem. We start by constructing a set of facts F 1 as before from f to complete F 0 , replacing the C-facts in the gadgets by S-facts. Now, we complete S + to add the transitive closure of these paths (note that they are disjoint from any other S-fact), and complete this to a set of facts to satisfy ⌃: create G-and G 0 -facts, and create gadgets, this time taking all of them to have length k + 1: this yields F 2 . We repeat this last process indefinitely on the path of S-facts created in the gadgets of the previous iteration, and let F be the result of this infinite process, which satisfies ⌃.

We justify as before that Q has no matches: as we create no S 0 -facts in F i for all i > 1, it suffices to observe that no new matches of Q can include any of the new facts, because each disjunct includes an S 0 -fact. Hence, we can conclude as before.

From UCQ to CQ. To prove the result with a CQ rather than a UCQ, we proceed as for the proof of Theorem 5: we extend S 0 to be a ternary relation with a propagated value, add the relations of Or (see the definition in the proof of Theorem 5), modify the S 0 -atoms in all disjuncts of the UCQ Q to add the variable, connect them as before yielding the CQ Q 0

, and modify the initial instance to add dummy matches, to add the element t to the S 0 -facts that we create, and to add the facts of F Or . As before, the proof of the forward direction is unchanged except that we add the value t to all S 0 -facts, and chase on the vacuous matches to satisfy the constraints (recall Definition 1). The query is violated because, thanks to the S 0 contained in each disjunct of Q, any match of the query ensures that we have a match of a disjunct of Q on the part that corresponds to F 0 (not on the vacuous matches). For the backwards direction, we extract the tiling as before, and argue thanks to the vacuous matches that any violation of the tiling property would violate a UCQ of Q, and hence violate Q 0

. This concludes the proof.

I Undecidability results related to linear orders (from Section 6)

We first prove Theorem 10. Recall the statement: Theorem 10. There is a signature

= B t D
where D is a single strict linear order relation, a CQ Q on , and a set ⌃ of inclusion dependencies on B (i.e., not mentioning the linear order, so in particular base-covered), such that the following problem is undecidable: given a finite set of facts F 0 , decide QAlin(F 0 , ⌃, Q).

Proof. We first show the claim for a UCQ rather than a CQ.

As in the proof of Theorem 8, we fix an undecidable infinite tiling problem C, V, H, and will reduce that problem to the QAlin problem.

Definition of the reduction. We consider the signature consisting of two binary relations R and D (for "right" and "down"), k 1 unary relations K 1 , . . . , K k 1 (representing the colors), and one unary relation S (representing the fact of being a vertex of the grid -this is just to simplify things).

We put the following inclusion dependencies in ⌃:

• 8x S(x) ! 9y R(x, y) • 8x S(x) ! 9y D(x, y) • 8xy R(x, y) ! S(y)

• 8xy D(x, y) ! S(y)

We will use the following abbreviations:

• K 0 1 (x) stands for 9y x < y ^K1 (y) • K 0 k (x) stands for 9y x > y ^Kk 1 (y) • for all 1 < i < k, K 0 i (x) stands for 9yy 0 K i 1 (y) ^y < x ^x < y 0 ^Ki (y 0 ). Intuitively, the K 0 i describe the color of elements, which is encoded in their order relation to elements labeled with the K i .

We consider a UCQ formed of the following disjuncts (existentially closed):

• R(x, y) ^D(x, z) ^R(z, w) ^D(y, w 0 ) ^w < w 0 • R(x, y) ^D(x, z) ^R(z, w) ^D(y, w 0 ) ^w0 < w • for each (c, c 0 ) 2 H, R(x, y) ^K0 c (x) ^K0 c 0 (y) • for each (c, c 0 ) 2 V, D(x, y) ^K0 c (x) ^K0 c 0 (y) Intuitively, the first two disjuncts enforce a grid structure, by saying that going right and then down must be the same as going down and then right. The two other disjuncts enforce that there are no bad horizontal or vertical patterns.

Let us now present the reduction. Consider an instance c 0 , . . . , c n of the tiling problem. We construct a set of facts F 0 as follows:

• S(a 0 ), . . . , S(a

n ) • R(a i 1 , a i ) for 1  i  n • K i (b i ) for 1  i  k • for each i such that c i is the color C 1 , a i < b 1
• for each i such that c i is the color C k , a i > b k 1

• for each 1 < j < k and i such that c i is C j , b j 1 < a i and a i < b j Correctness proof for the reduction. Let us show that the reduction is sound. Let us first assume that the tiling problem has a solution f . We construct a counterexample F ◆ F 0 as a grid of the R and D relations, with the first elements of the first row being the a 0 , . . . , a n , and with the color of elements being coded as their order relations to the b j like when constructing I above. Complete the interpretation of < to a total order by choosing one arbitrary total order among the elements labeled with the same color, for each color. The resulting interpretation is indeed a total order relation, formed of the following: some total order on the elements of color 1, the element b 1 , some total order on the elements of color 2, the element b 2 , . . . , the element b k 2 , some total order on the elements of color k 1, the element b k 1 , some total order on the elements of color k.

It is immediate that the result satisfies ⌃. To see why it does not satisfy the first two disjuncts of the UCQ, observe that any match of R(x, y) ^D(x, z) ^R(z, w) ^D(y, w 0 ) must have w = w 0

, by construction of the grid in F. To see why it does not satisfy the other disjuncts, notice that any such match must be a pair of two vertical or two horizontal elements; since the elements can match only one K 0 c which reflects their assigned color, the absence of matches follows by definition of f being a tiling.

Conversely, let us assume that there is a counterexample F ◆ F 0 which satisfies ⌃ and violates Q. Clearly, if the first two disjuncts of Q are violated, then, for any element where S holds, considering its R and D successors that exist by ⌃, and respectively their D and R successors, we reach the same element. Hence, from a 0 , . . . , a n , we can consider the part of F defined as a grid of the R and D relations, and it is indeed a full grid (R and D edges occur everywhere they should). Now, we observe that any element except the b j must be inserted at some position in the total suborder b 1 < • • • < b k 1 , so that at least one predicate K 0 j holds for each element of the grid (several K 0 j may hold in case F has more elements than the b i that are labeled with the K i ). Choose one of them, in a way that assigns to a 0 , . . . , a n their correct colors, and use this to define a function f that extends a 0 , . . . , a n . We claim that this f indeed describes a tiling.

Assume by contradiction that it does not. If there are two horizontally adjacent values (i, j) and (i + 1, j) realizing a configuration (c, c 0 ) from H, by completeness of the grid there is an R-edge between the corresponding elements u, v in F. Further, by the fact that (i, j) and (i + 1, j) were given the color that they have in f , we must have K 0 c (u) and K 0 c (v) in F, so that we must have had a match of a disjunct of Q, a contradiction. The absence of forbidden vertical patterns is proven in the same manner. We add to our initial set of facts F 0 the facts of F Or as in the proof of Theorem 5. We construct the CQ from the original UCQ by the same process as in the proof of Theorem 5, and construct the initial sets of facts as in that proof as well.

We then argue that this QAlin problem with the UCQ is equivalent to the one with the CQ. For the forward direction, from a solution to the initial instance a 0 , . . . , a n of the tiling problem, we build a suitable F ◆ F 0 from the previously defined F by putting t as the last element of R-and D-facts. We complete the vacuous matches by chasing on them with the dependencies of ⌃ (as in the proof of Theorem 5; recall Definition 1), we define < arbitrarily on each vacuous match, arbitrarily between them, arbitrarily with f and t, and then as before on the true grid. To show that the query has no match, we first claim that any match of the query must be a match of one of the disjuncts where the free variable is bound to t. Indeed, this is clear by definition of the Or and True relations. Now, we claim that none of the disjuncts have such a match. Indeed, if one disjunct has such a match, it implies that all facts of the match (except the order facts) have t in the last position, and, as these facts are the same as in the original proof (up to the last element), the absence of match is for the same reason as in the original proof.

Conversely, let us consider a F ◆ F 0 satisfying ⌃ and violating the query. We first observe that, for any disjunct of the query, it has a match where the free variable is bound to f, as witnessed by the vacuous matches. Hence, if the query has no match, it must mean that none of the disjuncts has a match with the free variable bound to t. Indeed, if there were one, then, from this match, from the vacuous matches, and using the facts which we know are present in the table of Or and True, we would obtain a match of the entire query. Hence, restricting our attention to the facts of F 0 with t in their last position, using the fact that none of the disjuncts has a match there, we conclude as in the original proof.

Now recall the statement of Corollary 5:

Corollary 5. There is a signature

= B t D
where D is a single strict linear order relation, and a set ⌃ 0 of BaseFGTGD constraints, such that, letting > be the tautological query, the following problem is undecidable: given a finite set of facts F 0 , decide QAlin(F 0 , ⌃ 0 , >).

To prove Corollary 5 from Theorem 10, we take constraints ⌃ 0 that are equivalent to ⌃ ^¬Q, where ⌃ and Q are as in the previous theorem. Recall that ⌃ is a set of inclusion dependencies on B , and therefore are BaseFGTGDs. Hence, it only remains to argue that ¬Q can be written as a BaseFGTGD. Indeed, write Q as 9x '(x) and consider the constraint 8x('(x) ! 9y(y < y))

where < is the distinguished relation. Since < must be a strict linear order in QAlin, 9y(y < y) is equivalent to ? and this new constraint is logically equivalent to ¬Q. Moreover, this constraint is trivially in BaseFGTGD since there are no frontier variables. Hence, ¬Q can be written as an BaseFGTGD as claimed.

  2EXP-c coNP-c 2EXP-c coNP-c 2EXP-c BaseFGTGD in coNP 2EXP-c coNP-c 2EXP-c undecidable BaseCovFGTGD P-c 2EXP-c coNP-c 2EXP-c coNP-c 2EXP-c(a) Summary of QA results (for base-covered fragments, queries are also base-covered) of atoms respectively called the body and head of ⌧ .

B

  Transitive-closure friendly tree decompositions for BaseGNF (Proof of Proposition 1) Recall the statement of Proposition 1: Proposition 1. Every sentence ' in BaseGNF has transitive-closure friendly k-tree-like witnesses, where k  |'|.

ã

  = a 1 . . . a n , we often abuse notation and write [v, ã] for the tuple [v, a 1 ], . . . , [v, a n ]. The decoding of T is the set of -facts decode(T ) using elements {[v, a] : v 2 T and a 2 names(v)}, where we identify z 2 elems(F 0 ) with the unique [

  the transition function with directions Dir ✓ {0, 1, 1}, and ⌦ : Q ! P is the priority function with a finite set of priorities P ✓ N.The transition function maps a state and input letter to a positive boolean formula over Dir⇥Q (denoted B + (Dir⇥Q)) that indicates possible next moves for the automaton.

  Overall size. We have argued that each automaton has at most N states and the number of priorities at most linear in . It remains to argue that the overall size of A is at most exponential in | | • N . The size of the priority mapping is at most polynomial in N . The size of the alphabet is exponential in | | • K k , which is at most exponential in | | • N . For each state and alphabet symbol, the size of the corresponding transition function formula can always be kept of size at most exponential in N . Hence, the overall size of the transition function is at most exponential in | | • N . Thus, the overall size of A is at most exponential in | | • N .

Lemma 4 .

 4 We can construct a 2-way alternating parity tree automaton A F0 in time doubly exponential in | | • K, such that for all trees T , A F0 accepts T iff T is consistent and for all facts S(c) 2 F 0 , decode(T ), [✏, c] satisfies S(x). when R + 2 D is interpreted as the transitive closure of R 2 B . The number of states is at most exponential in | |•K, the number of priorities is two, and the overall size is at most doubly exponential in | | • K.

Theorem 3 .

 3 For any BaseGNF constraints ⌃ and CQ Q, given a finite set of facts F 0 , we can decide QAtc(F 0 , ⌃, Q) in CoNP data complexity. Fix the signature . For a set of -facts F, an F, k-rooted structure is one that consists of F unioned with sets of facts T c for c 2 Dom(F) k where the domain of T c overlaps with the domain of F only in c, the facts of T c involving only elements of c are all present in F, and for two k-tuples c and c0 , the domain of T c overlaps with the domain of T c0 only within c \ c0 . The following proposition follows from Proposition 1. Proposition 14. For any set of -facts F, if a BaseGNF sentence ⌃ over is satisfiable by some set of facts containing F with relations R + i interpreted as the transitive closure of R i , then ⌃ is satisfied (with the same restriction) in an F 0 , krooted structure, where k is at most | | and F 0 is a superset of F that has the same domain. Let FO( ) denote first-order logic over the signature . Let FO( [{d 1 . . . d k }) denote first-order logic over the signature extended with k new constants, which will be used to represent the overlap elements. Note that formulas in both FO( ) and FO( [ {d 1 . . . d k }) can make use of distinguished R + i relations that are part of .

  Formally, define a signature Or with a ternary relation Or and a unary relation True. Define a set of facts F Or with two domain elements t and f that contains the fact True(t) and the facts Or(b, b 0 , b 00 ) for all {(b, b 0 , b _ b 0 ) | b, b 0 2 {f, t}}. Define 00 from 0 by increasing the arity of each relation in 0 except E and E + and adding the relations from Or . Define ⌃ 00 from ⌃ 0 by adding a new variable b which is universally quantified and is put in the head and body facts.

From

  UCQ to CQ. We now adapt the previous proof to use a CQ rather than a UCQ. Define the new signature 0 Or as in the proof of Theorem 5 by adding the relations of Or , and otherwise increasing the arity of each relation of B by one. Rewrite the IDs ⌃ as in the proof of Theorem 5, yielding: • 8x S(x, b) ! 9y R(x, y, b) • 8x S(x, b) ! 9y D(x, y, b) • 8xy R(x, y, b) ! S(y, b) • 8xy D(x, y, b) ! S(y, b)

  1 , f 1 , . . . , dn , e n , f

	n
	such V i R 0 i (c, di , e that is the transitive closure of E in F 0 witness ⌧ (c, d1 , e 1 , f 1 , . . . , dn , e i , f i ) ^E+ (e i , f i ). Moreover, since E + n , f n ) and

Acknowledgments

Amarilli was partly funded by the Télécom ParisTech Research Chair on Big Data and Market Insights. Bourhis was supported by CPER Nord-Pas de Calais/FEDER DATA Advanced Data Science and Technologies 2015-2020 and the ANR Aggreg Project ANR-14-CE25-0017, INRIA Northern European Associate Team Integrated Linked Data. Benedikt's work was sponsored by the Engineering and Physical Sciences Research Council of the United Kingdom (EPSRC), grants EP/M005852/1 and EP/L012138/1. Vanden Boom was partially supported by EPSRC grant EP/L012138/1.

• If t 1 and t 2 are both in F 1 , we reason as in the second case above.

• If t 1 lies in T c1 , t 2 lies in T c2 , then t 1 reaches some c i , c i 2 c1 , c i reaches some c j 2 c2 , and c j reaches t 2 within T c2 . Then we use a combination of the first two cases above to conclude that F is preserved.

From Lemma 8 we easily obtain: Corollary 6. Given ' and k there is a number j and a sentence ' 0 in the language of j-abstractions over such that for all sets of facts F, an F, k-rooted structure satisfies ' iff its j-abstraction satisfies ' 0 .

We can now put these results together to prove Theorem 3: Proof. Fixing Q and ⌃, we give an NP algorithm for the complement. Let ' = ⌃ ^¬Q, and k = |'|. Let j and ' 0 be the number and formula guaranteed for ' by Corollary 6.

Let FO( [ {d 1 . . . d k }) denote first-order logic over the signature of ⌃ ^¬Q, together with k constants.

Let Types j be the collection of assignments of truth values to all FO( [ {d 1 . . . d k }) sentences with quantifier-rank at most j such that the conjunction of the corresponding sentences is consistent. Note that the set is finite since j and the signature are fixed.

Given F, guess an extension F 0 with additional facts but the same domain. Guess a function f mapping each k-tuple over F to a ⇢ 2 Types j , and then for each

of quantifier rank at most j, interpret P ⌧ by the set of tuples c such that ⌧ 2 f (c). Check whether F 0 satisfies ' 0 with these interpretations, and if so return true. We argue for correctness. If the algorithm returns true with F 0 the witness, then create an F 0 , k-rooted structure A by picking for each c a structure satisfying the sentences in f (c) with distinguished elements interpreted by c (such a structure exists by consistency of f (c)), and letting the remaining domain elements be disjoint from the domain of F 0 . Note that by construction, A has F 0 as its j-abstraction. By the choice of j and ' 0

, and the observation above, A satisfies ⌃ ^¬Q. Thus this structure witnesses that QAtc(F, ⌃, Q) is false.

On the other hand, if QAtc(F, ⌃, Q) is false, then by Proposition 14 we have an extension F 0 without adding values to the domain, and an F 0 , k-rooted structure A that satisfies ⌃ ^¬Q. By the choice of j and ' 0 , the j-abstraction of A satisfies ' 0

. For each c in the j-abstraction of A, the type of c must be in Types j . Hence we can guess collections such that the algorithm returns true.

F.2 Proof of Theorem 4: PTIME data complexity bound for QAtr

We now turn to the case where our constraints are restricted to BaseCovFGTGDs and deal with QAtr, not QAtc. Recall that Theorem 4 states a PTIME data complexity bound for this case: Theorem 4. For any fixed BaseCovFGTGD constraints ⌃ and base-covered UCQ Q, given a finite set of facts F 0 , we can decide QAtr(F 0 , ⌃, Q) in PTIME data complexity.

The proof will follow from a reduction to traditional QA, similar to the proof of Proposition 3: Proposition 15. For any finite set of facts F 0 , constraints ⌃ 2 BaseCovGNF, and base-covered UCQ Q, we can compute F 0 0 and ⌃ 0 2 GNF in PTIME such that QAtr(F 0 , ⌃, Q) iff QA(F 0 0 , ⌃ 0 , Q). Furthermore, if ⌃ is in BaseCovFGTGD then ⌃ 0 is in FGTGD.

Proof. We define F 0 0 and ⌃ 0 as follows: • F 0 0 is F 0 together with facts G(a, b) for every pair a, b 2 elems(F 0 ) for some fresh binary base relation G, and