Mixed-World Reasoning with Existential Rules under Active-Domain Semantics

1 Introduction

There has been significant interest in recent years in ontologymediated query answering (OMQA) [Bienvenu and Ortiz, 2015], in which data is enriched with an ontology that provides general domain knowledge. Ontologies are typically expressed using decidable fragments of first-order logic. While description logics (DLs) [Baader et al., 2003] remain the most widely-studied formalism, existential rules (aka Datalog +/-) [Baget et al., 2009; Baget et al., 2011; Kr¨otzsch and Rudolph, 2011; Cal`ı et al., 2012], which we adopt in this paper, have been drawing increasing interest, as they allow relations of arbitrary arity (unlike DLs which are restricted to unary and binary predicates) and generalize both Datalog [Abiteboul et al., 1995] and tractable DLs like DLLite and EL [Calvanese et al., 2007; Baader et al., 2005].

The vast majority of work on OMQA adopts the open world assumption, whereby facts that are not present in the data instance are treated as unknown. Formally, each knowledge base (KB) (R, I), consisting of an ontology R and instance I, gives rise to a set of models, defined as the first-order structures that make true all facts in I and satisfy all rules (or axioms) in R. When querying a KB, we are interested in obtaining the certain answers, i.e. the answers that hold for every model of the KB. By contrast, relational databases make the closed-world assumption, where each instance I is interpreted as the finite structure whose domain is equal to the active domain of I (i.e., the constants explicitly mentioned in I) and which makes true precisely the facts in I.

In practice, it seems natural to assume that applications may involve some predicates whose contents are fully known and others for which we have only partial information. This motivates the consideration of mixed-world semantics, where the set of predicates is partitioned into closed and open predicates, and models are required to coincide with the instance on the closed predicates. Mixed-world OMQA was first explored for DL ontologies [Lutz et al., 2013; Lutz et al., 2015; Ahmetaj et al., 2016; Ngo et al., 2016] and has only recently been studied for existential rules [Benedikt et al., 2016]. Further variants of traditional OMQA semantics can be obtained by placing additional restrictions on the models. In particular, as the classical semantics considers arbitrary models with possibly infinite domains, it is interesting to consider the restriction to finite models [Ib´a˜nez-Garc´ıa et al., 2014; Gogacz et al., 2018] , or models with fixed or bounded-size domains [Gaggl et al., 2016; Rudolph and Schweizer, 2017].

The present paper combines elements of these different lines of research by exploring OMQA with existential rules under a hybrid mixed-world active-domain semantics, in which we can use both closed and open predicates, and the semantics is based upon active-domain models whose domains are equal to the active domain of the instance. Such a semantics is appropriate for scenarios in which all relevant constants are made available in the instance. A possible use case (formalized in Example 1 in simplified form), which served as a motivation for this work, is in analyzing the trajectories of people circulating in a geographically restricted area (e.g., industrial facility, closed medical facility) that is equipped with sensors and secure entry and exit (so that the set of people in the area is known at each timepoint).

The paper is structured as follows. In Section 3, we formally introduce our framework for mixed-world reasoning with existential rules under active-domain semantics, in particular, defining the certain and possible answers to conjunctive queries (CQs). In the following section, we analyze the data complexity of the three central reasoning tasks which are to determine whether a mixed-world knowledge base (MWKB) is satisfiable, and whether a Boolean CQ is certain or possible w.r.t. a MWKB. We show that all three tasks are intractable (NP- or coNP-complete in data complexity) for MWKBs based upon arbitrary existential rules. However, for the linear fragment of our language (where rule bodies may contain at most one atom with an open predicate), we are able to establish several tractability results. Indeed, we can show that satisfiability, possibility of BCQs, and certainty are all PTIME-complete in data complexity, and moreover, the PTIME upper bounds remain valid in the presence of useful extensions, like (in)equality atoms, negated closed atoms, and disjunction in ruleheads. Motivated by these encouraging results, we investigate the linear fragment in more detail. In Section 4, we explore the expressive power of the linear fragment and prove our most technically challenging result, namely, that atomic queries coupled with mixed-world linear existential rules, extended with either closed negated atoms or disjunctive ruleheads and interpreted under either certain or possible active-domain semantics, can express all PTIME queries over ordered databases. Section 5 provides a general method of approximating unrestricted existential rules by means of linear rules augmented with a fixpoint semantics. We conclude the paper with a discussion of related and future work. Due to space restrictions, some proof details have been deferred to the appendix of the long version [Bienvenu and Bourhis, 2019].

2 Preliminaries

We assume the reader is familiar with standard notions from first-order logic. A term is either a constant or variable. An atom takes the form P(t1, . . . , tk), where P is a predicate (or relation) symbol of arity k ≥ 0, and each ti is a term. A fact is an atom that does not contain any variables, and an instance is a finite set of facts. The active domain of an instance I, denoted adom(I), is the set of constants occurring in I.

A signature Σ is a finite set of predicate symbols. A Σinstance (resp. Σ-atom, Σ-fact) is an instance (resp. atom, fact) that only mentions predicates from Σ. The projection of an instance I onto Σ, denoted I|Σ, is the set of Σ-facts in I. When S is a set of instances, we let S|Σ = {I|Σ | I ∈ S}.

A conjunctive query (CQ) is a conjunction of atoms in which some of the variables may be existentially quantified. Atomic CQs consists of a single atom, and Boolean conjunctive queries (BCQs) are CQs whose variables are all existentially quantified. We use vars(Q) to denote the set of variables in a CQ Q. We sometimes treat (B)CQs as sets of atoms, e.g., using α ∈ Q to say that α occurs as a conjunct of Q.

We recall that an existential rule (sometimes abbreviated to rule) is a first-order sentence of the form ρ = ∀⃗xϕ(⃗x) → ∃⃗yψ(⃗x, ⃗y), where ϕ(⃗x) and ∃⃗yψ(⃗x, ⃗y) are CQs (called respectively the body and head of ρ), and all variables in ⃗x occur in ϕ(⃗x). An (existential) ruleset (over Σ) is a finite set of existential rules (whose predicates are drawn from Σ). For brevity, we omit the initial universal quantifiers in rules, use commas in place of ∧, and sometimes simplify to just ϕ → ψ (in which case the variables in vars(ψ) \ vars(ϕ) are implicitly existentially quantified). As is common, we shall assume that ruleheads always consist of a single atom. This is w.l.o.g. since we can simulate conjunctive ruleheads by means of fresh predicates, obtaining a ruleset that is a conservative extension of the original one.

Existential rules are classically interpreted under first-order logic semantics. An existential rule ϕ → ψ is satisfied in a first-order structure J with domain D if every variable assignment h : vars(ϕ) → D that makes ϕ hold in J can be extended to an assignment h′ : vars(ϕ) ∪ vars(ψ) → D such that ψ holds in J. We can extend the notion of satisfaction to instances as follows. With every instance I, we associate a finite first-order structure JI whose domain is adom(I) and such that every predicate P is interpreted as the set of tuples ⃗c such that P(⃗c) ∈ I. We then say that rule ρ is satisfied in an instance I (or that I satisfies ρ) if ρ is satisfied in JI. Likewise, a BCQ Q holds in instance I if Q holds in JI .

Datalog rules are existential rules with no existentially quantified variables, and a Datalog program is a finite set of Datalog rules. It is typical to partition the signature into extensional predicates that occur only in rule bodies, and intensional predicates that may occur both in bodies and heads. Given a Datalog program Π and an instance I over its extensional predicates, we denote by Π(I) the minimal instance that contains I and satisfies all rules in Π. A Datalog query takes the form (Π,Goal), where Π a Datalog program and Goal an intensional predicate. When evaluated on instance I, such a query returns those tuples ⃗a such that Goal(⃗a) ∈ Π(I). The preceding notions naturally extend to semi-positive Datalog, which allows negated extensional atoms in rule bodies.

3 Existential Rules with Closed Predicates and Active-Domain Semantics

This section introduces a framework for reasoning with existential rules in a setting where some of the predicates are declared as closed, and for the remaining open predicates, an active domain semantics is adopted, whereby only facts over the explicitly named constants are considered.

Formally, we will consider mixed-world signatures Σ = (Σc,Σo), whose predicates are partitioned into a set Σc of closed predicates, and a set Σo of open predicates. Often we will only define Σc, leaving it implicit that all other predicates in Σ belong to Σo. A mixed-world knowledge base (MWKB) is a triple (Σ,R, I), where Σ is a mixed-world signature, R is an existential ruleset over Σ, and I is a Σ-instance. Note that R and I may use both open and closed predicates. Later in the paper, we will be especially interested in linear existential rules, which we define in our setting as existential rules whose bodies contain at most one Σo-atom (but can contain any number of Σc-atoms 1 ).

We now define the active-domain (AD) semantics of MWKBs. A Σ-instance M is an active-domain model of a MWKB (Σ,R, I) if adom(M) = adom(I), M|Σc = I|Σc , I|Σo ⊆ M, and M satisfies every rule in R. The set of active-domain models (henceforth abbreviated to models) of (Σ,R, I) is denoted ModsAD(Σ,R, I). A MWKB (Σ,R, I) is satisfiable under AD semantics if ModsAD(Σ,R, I) ̸= ∅. There are two natural ways of interpreting queries in our setting:

1 Linear existential rules [Cal`ı et al., 2012] are usually restricted to a single body atom. Our definition is more general and in the spirit of linear Datalog rules [Abiteboul et al., 1995].

• a BCQ Q is certain w.r.t. (Σ,R, I) (under AD semantics) if Q holds in everyM ∈ModsAD(Σ,R, I);
• a BCQ Q is possible w.r.t. (Σ,R, I) (under AD semantics) if Q holds in some M ∈ ModsAD(Σ, R, I).

We extend these notions to arbitrary CQs in the obvious way: a tuple ⃗a of constants from adom(I) is a certain (resp. possible) answer to a CQ Q(⃗x) with free variables ⃗x iff the BCQ Q(⃗a) obtained by replacing ⃗x by ⃗a is certain (resp. possible). Observe that a BCQ Q is not possible just in the case that its negation ¬Q holds in every model, so the reasoning task of determining whether a BCQ is possible can be rephrased as determining whether a BCQ is certainly false. Note that because open predicates can be constrained by the closed predicates, not all open facts are possible (hence, some queries involving open predicates may be certainly false).

We will also consider a more general form of existential rule that allows for the following useful features: (in)equality atoms (t = t′ , t ̸= t′ ) in rule bodies and heads, negated Σcatoms in rule bodies, and rule heads that take the form of a (possibly empty) disjunction of existentially quantified atoms. We will call these extended (existential) rules. An extended linear rule is an extended rule with at most one Σo-atom in its body, where (in)equality atoms are viewed as Σc-atoms. The notion of an extended rule holding in an instance is defined in the obvious way, following first-order logic semantics.

We conclude this section by an example that illustrates the use of our logic to reconstruct trajectories of users whose positions are recorded by different sensors in an area.

Example 1. The goal is to reconstruct paths of people circulating in a circumscribed area based upon sensor events. Every such event has an identifier e and provides the position p of a (possibly unidentified) user u at a certain time t. Nominative events are stored as facts N(e, p, t, u), and all events (both nominative and anonymous) are stored as facts E(e, p, t) in a generic event relation E. For the purposes of the example, we assume events occur at regular intervals (every ∆t time units), and every user participates in some event (e.g., is detected by some sensor) at each timepoint (if this event identifies the user, then it is nominative, else anonymous). We further assume that Next contains all pairs of events (e, e′ ) that can feasibly occur in sequence i.e., the timepoint of e′ directly follows that of e, and it is physically possible to move between their respective positions in ∆t. Finally, we assume special nominative events containing the starting and ending positions of a user in the considered area, which can be found in relations S and F. Based upon the preceding information (stored in closed predicates), we construct possible trajectories by means of an open predicate T r, where Tr(u, e, e′ ) means that user u transitions from event e to event e′ ; a second open predicate Loc(u, p, t) states that u is at position p at time t. Our first two rules guess a subsequent event for every event up to the final event (note that the variable e′′ with the guessed event is existentially quantified):

We use Next to constrain the pairs of events in Tr,

and enforce that if the true position of a user is known at a given timepoint t (via a nominative event), then any selected event for that user at time t gives the same position:

Loc-facts record the times and position of events in the guessed trajectories given by relation Tr:

and the final two rules forbid a user from being in more than one position at a time, and for distinct users being associated to the same position at the same time:

The first five rules are linear, while the last two are not. The certain (resp. possible) Loc-facts provide us with the sure (resp. potential) location of users at different timepoints, which could be used for visualizing and analyzing user trajectories. For example, displaying (or aggregating) the certain and possible locations of users (given by Loc) could help with understanding which sectors are the most frequented.

4 Complexity Analysis

We study the complexity of the three main reasoning tasks in our setting: satisfiability, certainty, and possibility. We focus on data complexity, which is measured in terms of the size of the instance. Our results are formulated for BCQs, but they apply equally well to the decision problem of testing whether a given tuple is a certain / possible answer.

Our first result shows that reasoning in the full language is intractable in data complexity, which is not surprising in light of prior negative results for mixed-world reasoning.

Theorem 1. For (possibly extended) MWKBs with AD semantics, deciding if a BCQ is certain is coNP-complete in data complexity, while KB satisfiability and BCQ possibility are NP-complete in data complexity. The lower bounds hold for binary signatures and when the BCQ is a fact.

Proof sketch. We focus on certainty, but the proofs are easily adapted for satisfiability and possibility. To show q is not certain w.r.t. (Σ,R, I), it suffices to guess an instance J with adom(J) = adom(I), and verify that I|Σo ⊆ J, J coincides with I on Σc, all rules in R are satisfied in J, and q does not hold in J. As J is of polynomial size in |I|, and we can verify rule satisfaction in PTIME w.r.t. |J|, we get an NP upper bound (data complexity) for non-certainty.

For the lower bound, we adapt a reduction from 2+2UNSAT sketched in [Lutz et al., 2013]. Let R2+2 consist of:

• for i ∈ {1, 2}: Pi(x, y)→ ∃zR(y, z), Pi(x, y), R(y, z), F (z) → Ui(x)
• for i ∈ {3, 4}: Ni(x, y)→ ∃zR(y, z), Ni(x, y), R(y, z), T (z) → Ui(x)
• R(y, x)→B(x)
• (S(w, x), ∧1≤i≤4 Ui(x)) →Q(w)

Given a CNF ϕ = λ1, . . . , λn with λi = vi1 ∨vi2 ∨¬vi3 ∨¬vi4 , we construct the following instance I2+2:

It is easily verified that, letting Σc = {B}, the fact Q(a) is certain for (Σ,R2+2, I2+2) iff ϕ is unsatisfiable.

We next turn to linear rulesets. A straightforward adaptation of Theorem 1 shows that linearity does not always yield tractability, even for normally well-behaved classes of BCQs:

Theorem 2. For linear MWKBs with AD semantics, deciding if an acyclic 2 BCQ is certain is coNP-hard in data complexity.

Proof sketch. We adapt the reduction from Theorem 1 by (i) using the acyclic BCQ obtained by 'unfolding' Q(a) w.r.t. the rules with head predicates Q and Ui, and then (ii) removing all non-linear rules from the ruleset R2+2.

Nevertheless, we can show several positive results for linear rules, exploiting the following maximal model property:

Lemma 1. Consider a signature Σ = (Σc,Σo), an extended linear ruleset R over Σ, and Σ-instances I,N with adom(N) ⊆ adom(I). If {M ∈ ModsAD(Σ,R, I) | M ∩ N = ∅} is non-empty, then it has a maximal element w.r.t. set inclusion, called the maximal model of (Σ,R, I) that omits N. Moreover, computing this model (or determining its non-existence) can be done in polynomial time in |I|.

Proof. We outline a procedure for testing whether there is a model of (Σ,R, I) that omits N, and constructing the maximal such model when it exists. If N∩I ̸= ∅, then we immediately fail. Otherwise, we set J equal to the (unique) maximal Σ-instance with adom(J) = adom(I) and J ∩ N = ∅ that coincides with I on Σc. If J satisfies R, then we have found the desired maximal model. Otherwise, repeat the following while J does not satisfy R:

1. Pick a rule γ → ψ that is not satisfied in J, together with a variable assignment h : vars(γ) → adom(J) such that h(γ) is satisfied in J but there is no extension h′ of h to vars(γ) ∪ vars(ψ) such that h′ (ψ) holds in J.
2. If γ contains an atom P(⃗x) with P ∈ Σo and P(h(⃗x)) ̸∈ I, then remove P(h(⃗x)) from J.
3. Else, halt and return 'no such model'.

If at some point J satisfies R, halt and return J.

Correctness of this procedure can be established by an inductive argument, which shows that the current set J is always a superset of the desired maximal model if it exists (intuitively because every fact removal is 'forced'). Note that the initial J can be constructed in polynomial time in |I|, and there at most polynomially many iterations of the above steps, so the procedure runs in PTIME w.r.t. data complexity.

As an immediate consequence of Lemma 1, we have:

2 We recall that a BCQ Q is acyclic if the undirected graph (VQ,EQ) is acyclic, where VQ contains the terms of Q, and EQ contains (t, t′ ) iff there is an atom of Q containing t and t′ .

Theorem 3. Satisfiability of extended linear MWKBs with AD semantics is in PTIME for data complexity.

We can also use Lemma 1 to identify classes of queries for which the certainty problem is tractable.

Theorem 4. For extended linear MWKBs with AD semantics, deciding if a fact is certain is in PTIME for data complexity. The same holds for ground CQs and for disjunctions of facts.

Proof sketch. To test whether fact α is not certain, it suffices to determine the existence of a model that omits N = {α}, a PTIME-checkable condition by Lemma 1. For a ground CQ α1 ∧. . .∧αn, we just perform this test for each αi separately. Finally, note that a disjunction of facts α1∨. . .∨αn is certain iff there is no model that omits {α1, . . . , αn}.

We now provide matching PTIME lower bounds for satisfiability and fact certainty. Recall that the latter problem is in AC0 ⊊ PTIME for linear existential rules under classical semantics without closed predicates [Cal`ı et al., 2012].

Theorem 5. For linear MWKBs with AD semantics, satisfiability and fact certainty are PTIME-hard in data complexity.

Proof sketch. The proof is by reduction from the PTIMEcomplete Path Systems Accessibility (PSA) problem [Garey and Johnson, 1979]. A path system is a tuple (U,E, S, t) where U is a set of nodes, E ⊆ U × U × U is an accessibility relation, S ⊆ U is the set of source nodes, and t ∈ U is the distinguished terminal node. The problem is then to determine whether t ∈ access(S), where access(S) is the least subset of U such that (i) S ⊆ access(S), and (ii) if u1, u2 ∈ access(S) and (u1, u2, u3) ∈ E, then u3 ∈ access(S).

Observe that u ∈ access(S) iff there is a labelled binary tree such that (i) the root is labelled u, (ii) every leaf is labelled by some u′ ∈ S, and (iii) for every non-leaf node with label u3, there is (u1, u2, u3) ∈ E such that the node's children are labelled u1 and u2. We remark that if such a witness tree exists, then there is one with depth is at most |E|. The idea for the reduction is to try to build such a witness tree.

Given a path system PS = (U, E, S, t) with |E| = m, we construct (by a logspace transducer) the instance IPS with:

• Init(t, 0), with t the unique terminal node
• R(u, u′ , u′′ , k, k + 1), for (u, u′ , u′′ ) ∈ E, 0 ≤ k < m
• R(u, u, u, k, k + 1), for each u ∈ S and 0 ≤ k < m
• R(u, u, u,m,m), for each u ∈ S

We set Σc = {Init, R}, and let RPS consist of the rules:

• Init(x, z) → ∃y1, y2, z′ T(y1, y2, x, z, z ′ )
• T(y1, y2, x, z, z ′ ) →R(y1, y2, x, z, z ′ )
• T(y1, y2, x, z, z ′ ) → ∃v1, v2, z′′T(v1, v2, y1, z′ , z′′ )
• T(y1, y2, x, z, z ′ ) → ∃v1, v2, z′′T(v1, v2, y2, z′ , z′′ )

The rough idea is that we guess a witness tree topdown, from the root t to the leaves, using the T-facts to record which triples from E were used. Correctness follows from the fact that every model of (Σ,RPS, IPS) gives rise to a witness tree for t ∈ access(S) (constructed from the T-facts), and conversely, every such tree can be used to build a model. The numbers occurring in the last two positions of T play a crucial role, by ordering the T -facts (allowing them to be assembled into a witness tree) and forcing each 'branch' to eventually stabilize in S (as once value m has been reached, we can only use T-facts of the form T(u, u, u,m,m) with u ∈ S). It follows that (Σ,RPS, IPS) is satisfiable iff t ∈ access(S). For certainty, we pick a fact α = Init(u, v) ̸∈ IPS and note that α is certain iff (Σ,RPS, IPS) is unsatisfiable.

For possibility, we obtain tractability for arbitrary BCQs:

Theorem 6. For (extended) linear MWKBs with AD semantics, BCQ possibility is PTIME-complete for data complexity. The lower bound holds when the BCQ is a fact.

Proof sketch. To decide if q is possible, it suffices to check whether q holds in the unique maximal model, which can be done in PTIME w.r.t. data complexity by Theorem 1.

The lower bound is by reduction from the PSA problem introduced earlier. The ruleset will consist of the following four linear rules, with Σc = {NR0, B, In, Out}:

The input (U, E, S, t) is encoded by the following instance:

• B(0), B(1), and NR0(u) for every u ∈ U \ S
• for every ei = (ui,0, ui,1, ui,2) ∈ E, the facts In(ei, 0, ui,0), In(ei, 1, ui,1), and Out(ei, ui,2)

It can be verified that u ∈ access(S) iff NR(u) is not possible for every u ∈ U, and in particular, when u = t, yielding a reduction from PSA to non-possibility.

5 Expressive Power of Linear Fragment

We now study mixed-world linear existential rules under AD semantics from the perspective of query expressivity.

We recall that from an abstract perspective, a k-ary query Q over a signature Σ is a function that maps every Σinstance I to a finite k-ary relation Q(I) (containing the query answers). A query is called generic if it is invariant under renaming of constants 3 , which implies in particular that adom(Q(I)) ⊆ adom(I). With every k-ary query Q over Σ, we can associate the following recognition problem: given a Σ-instance I and k-tuple ⃗a of constants from adom(I), decide whether ⃗a ∈ Q(I). The class QPTIME consists of all generic queries whose recognition problem is computable in polynomial time w.r.t. data complexity.

Finding a logical language that precisely captures QPTIME is a major open problem in descriptive complexity. The following well-known result shows that the class of semipositive Datalog queries captures QPTIME over so-called ordered instances with min and max, i.e., instances I with a binary predicate Succ providing a successor relation among all constants in adom(I), and unary predicates Min and Max containing the smallest and largest constants.

Theorem 7 ([Papadimitriou, 1985]). Over ordered instances with min and max, semi-positive Datalog captures QPTIME.

3 Queries that mention constants are not generic, but can be simulated using generic queries, see [Abiteboul et al., 1995] for details.

Interestingly, we can show that our linear fragment, extended with either closed negated atoms or disjunctive ruleheads and interpreted with either certain or possible semantics, captures QPTIME over ordered instances. Formally, the next theorem concerns the classes of queries obtained by associating with every constant-free atomic query A(⃗x) and extended linear existential ruleset R over Σ the (generic) queries QA,R,c and QA,R,p that map I respectively to the certain and possible answers of A(⃗x) w.r.t. (Σ, R, I).

Theorem 8. Over ordered instances, atomic queries coupled with mixed-world linear rulesets extended with either closed negated atoms or disjunctive ruleheads and interpreted under either the certain or possible AD semantics capture QPTIME.

In the remainder of this section, we outline the key steps in the proof of Theorem 8. We start by noting that differently from Theorem 7, our result does not require the instance to provide the values min and max. This is because we can show how to compute these values from Succ using our rules.

Suppose we are given a semi-positive Datalog program Π with extensional predicates ΣΠ ⊇ {Succ,Min,Max} and k-ary output relation Goal. The core of the proof will be concerned with constructing a set of extended linear existential rules RΠ over Σ with Σc = ΣΠ \ {Min, Max} such that for every ordered Σc-instance I and k-tuple of constants ⃗a, the following statements are equivalent:

1. Goal(⃗a) ∈ Π(I∪{Min(min),Max(max)}, withmin and max the smallest and largest constants in I
2. Ans(⃗a) is certain w.r.t. (Σ,RΠ, I)
3. Ans(⃗a) is possible w.r.t. (Σ,RΠ, I)

To simplify the construction, we initially let RΠ consist of linear rules extended with both negated closed predicates and disjunctive ruleheads. Then in a final step, we show how we can get rid either of negated atoms or disjunctions.

Let us describe at a high level the ruleset RΠ. We include rules that populate an open predicate Tuple with all k-ary tuples of constants from the active domain and then guess for each tuple, whether it is an answer to the Datalog query:

To verify that these guesses are correct, we rely upon the fact that α ∈ Π(J) iff there is a proof tree for α [Abiteboul et al., 1995], i.e., a tree whose root is labelled α, whose every leaf node is labelled with either an extensional fact β with β ∈ J or a negated extensional fact ¬β with β ̸∈ J, and such that for each non-leaf node with label β and whose children have labels γ1, . . . , γk, the ground rule γ1, . . . , γk → β can be obtained from a rule in Π by instantiating its variables with constants from adom(J). It is known that the depth of a minimal proof tree is bounded by p(|I|) for some polynomial function p. To verify Ans(⃗a), we follow a similar approach to the proof of Theorem 5 and guess a proof tree for Goal(⃗a) by working from root to leaves (failing if no such proof tree exists). To verify a fact NotAns(⃗a), we use a second set of rules to enforce that there is no proof tree for Goal(⃗a) of depth at most p(n). Essentially, we guess topdown a 'noproof' tree whose root is labelled Ans(⃗a), whose leaves are labelled by extensional facts not in J (here we used closed negated atoms) or negations of extensional facts from J, and such that for every non-leaf node ν with label β and every ground instantiation γ1, . . . , γk → β of a rule in Π, there is a child of ν that is labelled with some γi. We implement counters that keep track of the depth of the guessed trees and fail if we exceed p(n). By construction, (Σ,RΠ, I) is satisfiable. Moreover, while the models may differ on which trees are guessed, they always coincide on Ans and NotAns facts. It follows that Ans(⃗a) is certain iff it is possible iff Goal(⃗a) ∈ Π(I ∪ {Min(min), Max(max)}.

The rules implementing the preceding construction presume the existence of at least two values (min ̸= max), which are used to implement binary counters. Thus, we must identify instances containing a single constant (min = max) and create a separate set of rules to compute the answers in this limit case. Briefly, the idea is to create a dedicated rule for each single-constant instance, using negated closed atoms to identify the contents of the input single-constant instance.

To complete the proof, we show how to simulate negated closed atoms using disjunction in ruleheads, and conversely, how to simulate disjunctive ruleheads using negated closed atoms. The latter translation only works for instances with at least two constants, but this is sufficient for our purposes, as disjunction only occurs in the rules that fire on instances with multiple constants. We point out that if we were to restrict to the class of instances with at least two constants, then both transformations are applicable and yield (plain) linear rules.

6 Fixpoint Extension of Linear Fragment

While the (extended) linear fragment has desirable computational properties, it cannot express some useful constructs, such as functionality (cf. final rule from Example 1). In this section we show how arbitrary rulesets can be approximated via a fixpoint-style extension of the linear fragment.

The idea is as follows. Given an arbitrary ruleset R over Σ = (Σc, Σo), we can first compute the certain and possible facts using only the linear rules in R, which yields a subset of the 'true' certain facts and a superset of the possible ones. We store these facts in new closed predicates Rlb and Rub , use rules to link them to the original open predicates, create new linear rules from the non-linear rules by replacing all open atoms but one with closed Rlb -atoms, then recompute the certain and possible facts. Iterating this process until fixpoint allows us to obtain more refined approximations of the certain and possible facts of the original ruleset.

Formally, an (extended) linearfp ruleset over Σ = (Σc, Σo) is an (extended) linear ruleset over Σ+ = (Σ+c , Σo) where

and Rlb -atoms (resp. Rub -atoms) may only occur positively and in rule bodies (resp. ruleheads). Given such a ruleset R, we denote by R+ the ruleset

(with ⃗x a tuple of distinct variables of the same arity as R). These rules formalize that Rlb (resp. Rub ) places a lower (resp. upper) bound on the set of R-facts.

Given a linearfp ruleset R over Σ = (Σc,Σo) and a Σinstance I, we define inductively the set Modsk (Σ,R, I) of models of (Σ, R, I) at each stage k ≥ 1:

• Mods1 (Σ, R, I) = ModsAD(Σ+, R+, I0)|Σ, where I0 = I ∪ {Rub (⃗a) | R ∈ Σo of arity n,⃗a ∈adom(I)n }

where, for every k ≥ 1, the set Certk (Σ,R, I) (resp. Possk (Σ,R, I)) contains the Σ-facts over adom(I) that appear in every (resp. some) M ∈ Modsk (Σ,R, I). The next lemma shows that these sets eventually converge to a fixpoint.

Lemma 2. For every linearfp ruleset R over Σ and Σinstance I, Modsj+1 (Σ,R, I) ⊆ Modsj (Σ,R, I) for every j ≥ 1, and there exists k∗ ≥ 1 such that Modsj (Σ,R, I) = Modsk∗ (Σ,R, I) for every j ≥ k∗ .

Proof Sketch. We can show by simultaneous induction that (i) Certj-1 (Σ,R, I) ⊆ Certj (Σ,R, I), (ii) Possj (Σ,R, I) ⊆ Possj-1 (Σ,R, I), and (iii) Modsj+1 (Σ, R, I) ⊆ Modsj (Σ, R, I) for every j ≥ 1.

In what follows, we'll use Mods∞(Σ,R, I) to refer to the fixpoint Modsk∗ (Σ,R, I) from Lemma 2, and similarly for Cert∞(Σ,R, I) and Poss∞(Σ,R, I). We observe that the stage k∗ where the fixpoint is reached is bounded polynomially in |I|. When combined with Theorems 4 and 6, this yields the following tractability result:

Theorem9. The problems of decidingwhether a fact belongs to Cert∞(Σ, R, I) or to P oss∞(Σ, R, I) are both in PTIME for data complexity.

Next consider an extended existential ruleset R over Σ = (Σc,Σo). The linearization of R, denoted Rlin , is obtained by replacing each rule ε ∧ β1 ∧ . . . ∧ βm → γ ∈ R, whose body Σo-atoms are β1, . . . , βm, with the set of rules:

The following theorem shows that Rlin , under the above fixpoint semantics, provides an under-approximation of the certain facts and an over-approximation of the possible facts.

Theorem 10. Let R be an extended existential ruleset over Σ, and let Rlin be its linearization. For every Σ-instance I: ModsAD(Σ,R, I) ⊆ Mods∞(Σ,Rlin , I). In particular, this implies that for every fact α:

• α ∈ Cert∞(Σ, Rlin , I) ⇒ α is certain w.r.t. (Σ, R, I);
• α is possible w.r.t. (Σ, R, I) ⇒ α ∈ P oss∞(Σ, Rlin , I).

The next result shows that linearization provides a nontrivial approximation in the sense that in general there is no instance-independent bound on the number of iterations needed to reach the fixpoint.

Lemma 3. There exists a Σ-ruleset R such for every j ≥ 0, there is a Σ-instance I such that Modsj+1 (Σ,R, I) ̸= Modsj (Σ, R, I ).

Proof. Consider the following ruleset 4 Rsat:

• Clause(u) → SatLit(u, x, y)
• SatLit(u, x, y) →ClauseLit(u, x, y)
• SatLit(u, x, y) →PickV al(x, y)
• PickV al(x, y) →B(y)
• P ickV al(x, y) ∧ P ickV al(x, y′ ) → y = y′

With every CNF ϕ = c1 ∧ . . . ∧ cn over v1, . . . , vm, we associate the instance Iϕ consisting of the following facts:

• B(0),B(1)
• Clause(ci) for 1 ≤ i ≤ n
• ClauseLit(ci, vj, 1) if ci contains vj
• ClauseLit(ci, vj, 0) if ci contains ¬vj

We let Σsat contain all of the preceding predicates, where Clause,ClauseLit,B are the only closed predicates. It can be verified that (Σsat,Rsat, Iϕ) iff ϕ is satisfiable. Moreover, PickV al(pi, 1) (resp. PickV al(pi, 0)) is certain iff every satisfying valuation of ϕ sets pi to true (resp. false).

The linearization (Rlin sat )+ retains the first four rules of Rsat and adds new rules, the most relevant being:

• P ickV allb (x, y) ∧ P ickV al(x, y′ ) → y = y′
• PickV allb (x, y) →PickV al(x, y),
• PickV al(x, y) →PickV alub (x, y)

Consider the sequence of propositional CNF ξi (i ≥ 1), where ξi = c1 ∧ . . . ∧ ci, c1 = p1, and cℓ+1 = ¬pℓ ∨ pℓ+1 for 1 ≤ ℓ < i. As every ξi is satisfiable, we know that (Σsat,Rsat, Iϕ) is satisfiable. By Theorem 10, the same is true of (Σsat,Rlin sat , Iξi ). Moreover, ξi |= pℓ for every 1 ≤ ℓ ≤ i, so by the above, we have PickV al(pℓ, 1) ∈ Cert∞(Σsat, Rlin sat , Iξi ) for all 1 ≤ ℓ ≤ i. A simple inductive argument shows that for every i ≥ 1 and 1 ≤ k ≤ i:

Hence, if Certk (Σ+sat ,Rlin sat , Iξi ) = Cert∞(Σ+sat , Rlin sat , Iξi ), then k ≥ i. Thus, by considering ξi for increasing values of i, we can delay the achievement of the fixpoint, meaning it cannot be bounded independently of the instance.

A relevant question for future work is to analyze, either formally or experimentally, the quality of our approximation.

7 Concluding Remarks

In this paper, we investigated the problem of reasoning with existential rules under a hybrid mixed-world active-domain semantics. While querying in our setting is intractable in the general case, we identified an interesting and non-trivial fragment based upon linear rules that is PTIME-complete in data complexity, and in fact, captures all of QPTIME over ordered instances. To obtain a more widely applicable PTIME result, we provided a method of approximating non-linear rules by means of linear rules equipped with a fixpoint semantics.

4 We have used an equality atom for convenience, but it is possible to modify the proof so that it works in the basic formalism.

We point out that a PTIME upper bound for possible BCQs with mixed-world semantics has been shown in [Benedikt et al., 2016; Benedikt et al., 2018] for a more restricted notion of linear rule (and without PTIME-hardness and QPTIME results). The key difference with [Benedikt et al., 2018] and other works on mixed-world reasoning [Lutz et al., 2013; Lutz et al., 2015; Ahmetaj et al., 2016; Ngo et al., 2016] is that we adopt active-domain semantics, whereas these other works use classical semantics under which new values can appear in the open predicates. This has a very significant impact on the decidability and complexity of reasoning. For example, certainty of BCQs is decidable in our setting even for arbitrary existential rules, while it is undecidable under classical semantics; for frontier-guarded rules, certainty of BCQs was shown to be EXPTIME-complete in data complexity [Benedikt et al., 2016], while it is coNP-complete in data complexity for our setting. A notable similarity is that our PTIME membership results employ a greatest fixpoint construction, which is in the same spirit as techniques used in [Benedikt et al., 2018; Benedikt et al., 2016]. Other non-trivial data tractability results have been obtained for fact certainty in the presence of linear disjunctive Datalog rules [Kaminski et al., 2016], and for exact views given as LAV source-to-target rules [Benedikt et al., 2018].

The present work can be continued in several directions. First, we can study the combined complexity of reasoning in our setting for different classes of existential rules, and the impact of using a fixed but succinctly represented domain, in the spirit of [Rudolph and Schweizer, 2017]. There are also many interesting questions related to expressive power and the (non)existence of translations to various Datalog extensions (e.g, disjunctive Datalog [Eiter et al., 1997], or Datalog with non-deterministic choice [Abiteboul and Vianu, 1991]). We note that polynomial translations to disjunctive Datalog with negation have been proposed to compute certain facts w.r.t. mixed-world KBs in expressive description logics [Ahmetaj et al., 2016], and a similar approach may be worth exploring in our setting. On the practical side, we have already begun applying our framework to integrating geolocalization data as illustrated by our example. Here the main challenge is to develop more efficient PTIME algorithms that do not require the construction of full maximal models, which although polynomial may be impractical for large domains. We would also like to allow for closed relations that are implicitly defined by PTIME-computable functions (e.g., Next from Example 1 that could be defined using distances between locations) that are not computed and stored in advance but rather produced as needed.

Acknowledgements

We thank the reviewers for their detailed and constructive feedback. This work was partially supported by CNRS Momentum project "Managing Data without Leaks" and ANR project CQFD (ANR-18-CE23-0003).