The Datalog family of expressive extensions of Datalog has recently been introduced as a new paradigm for query answering over ontologies, which captures and extends several common description logics. It extends plain Datalog by features such as existentially quantified rule heads and, at the same time, restricts the rule syntax so as to achieve decidability and tractability. In this paper, we continue the research on Datalog . More precisely, we generalize the well-founded semantics (WFS), as the standard semantics for nonmonotonic normal programs in the database context, to Datalog programs with negation under the unique name assumption (UNA). We prove that for guarded Datalog with negation under the standard WFS, answering normal Boolean conjunctive queries is decidable, and we provide precise complexity results for this problem, namely, in particular, completeness for PTIME (resp., 2-EXPTIME) in the data (resp., combined) complexity.
The recent Datalog family of ontology languages [
The Datalog languages bridge an apparent gap in expressive power between database
query languages and DLs as ontology languages, extending the well-known Datalog
language in order to embed DLs. They also allow for transferring important concepts and proof
techniques from database theory to DLs. For example, it was so far not clear how to enrich
tractable DLs by the feature of nonmonotonic negation. By the results of [
Given that stratified negation is quite limited, it is natural to ask whether the richer and
more expressive well-founded negation could be defined for Datalog . The well-founded
semantics (WFS) for normal (logic) programs [
In [
The WFS for normal Datalog without the UNA, however, actually generalizes neither
Datalog nor standard normal (logic) programs, which make the UNA, in contrast. The UNA
is also rather common in logic programming and databases in general, as well as in some
important DLs, such as the DL-Lite family of tractable description logics [
The first rule expresses that an employed person who is not registered as a job seeker has an
employee’s ID, the second rule states that a person who is not employed, and does not have an
employee’s ID is registered as a job seeker, and the final rule expresses that IDs are only valid,
if they are not an employee’s and a job seeker’s ID simultaneously. As pointed out in [
Another serious drawback of the equality-friendly WFS is that answering atomic queries is co-NP-hard in the data complexity, and thus does not have the same nice computational properties as in the standard WFS for normal logics programs, namely, a polynomial data complexity. The development of a WFS for normal Datalog under the UNA (with hopefully lower data complexity than the WFS without the UNA) is thus still an important open problem, which we therefore tackle in the present paper.
The central question of this paper is whether the results for guarded positive Datalog
from [
As the main contributions of this paper, we thus obtain that answering NBCQs to guarded
normal Datalog under the WFS and UNA is decidable and can be done in polynomial time
in the data complexity. Furthermore, we show that it is in 2-EXPTIME in the combined
complexity in general and in EXPTIME in the combined complexity in the case where the
arities of all predicates are bounded by a constant. Hardness for these complexity classes
follows from the fact that already answering BCQs to the more restricted guarded Datalog
without negation is hard for them. Note that an extended version of this paper is accepted for
publication in: Proceedings PODS-2013 [
Databases and Queries We assume (i) an infinite universe of (data) constants (which constitute the “normal” domain of a database), (ii) an infinite set of (labeled) nulls N (used as “fresh” Skolem terms, which are placeholders for unknown values, and can thus be seen as variables), and (iii) an infinite set of variables V (used in queries and dependencies). Different constants represent different values (unique name assumption), while different nulls may represent the same value. We assume a lexicographic order on [ N , with every symbol in N following all symbols in . We denote by X sequences of variables X1; : : : ; Xk with k > 0.
We assume a relational schema R, which is a finite set of relation names (or predicate symbols, or simply predicates). A term t is a constant, null, or variable. An atomic formula (or atom) a has the form P (t1; :::; tn), where P is an n-ary predicate, and t1; :::; tn are terms. We denote by pred (a) and dom(a) its predicate and the set of all its arguments, respectively. The latter two notations are naturally extended to sets of atoms and conjunctions of atoms. A conjunction of atoms is often identified with the set of all its atoms.
A database (instance) D for a relational schema R is a (possibly infinite) set of atoms with predicates from R and arguments from . A conjunctive query (CQ) over R has the form Q(X) = 9Y (X; Y), where (X; Y) is a conjunction of atoms with the variables X and Y, and eventually constants, but without nulls. Note that (X; Y) may also contain equalities but no inequalities. A Boolean CQ (BCQ) over R is a CQ of the form Q(). We often write a BCQ as the set of all its atoms, having constants and variables as arguments, and omitting the quantifiers. Answers to CQs and BCQs are defined via homomorphisms, which are mappings : [ N [ V ! [ N [ V such that (i) c 2 implies (c) = c, (ii) c 2
N implies (c) 2 [ N , and (iii) is naturally extended to atoms, sets of atoms, and conjunctions of atoms. The set of all answers to a CQ Q(X) = 9Y (X; Y) over a database D, denoted Q(D), is the set of all tuples t over for which there exists a homomorphism : X [ Y ! [ N such that ( (X; Y)) D and (X) = t. The answer to a BCQ Q() over a database D is Yes, denoted D j= Q, iff Q(D) 6= ;. 2.2
Normal Logic Programs We now briefly recall standard normal logic programs. Let be a first-order vocabulary with nonempty finite sets of constant, function, and predicate symbols. Let V be a set of variables. A term is either a variable from V, a constant symbol from , or of the form f (t1; : : : ; tn), where f is a function symbol of arity n > 0 from , and t1; : : : ; tn are terms. An atom has the form p(t1; : : : ; tn), where p is a predicate symbol of arity n > 0 from , and t1; : : : ; tn are terms. A literal l is an atom p or a negated atom :p. A (normal) rule r is of the form 1; : : : ; n; : n+1; : : : ; : n+m ! ; (1) where ; 1; : : : ; n+m are atoms and m; n > 0. We call the atom the head of r, denoted H(r), while the conjunction 1; : : : ; n; : n+1; : : : ; : n+m is called its body. We define B(r) = B+(r) [ B (r), where B+(r) = f 1; : : : ; ng and B (r) = f n+1; : : : ; n+mg. A rule of the form (1) with m = n = 0 is also called a fact. A normal program P is a finite set of normal rules (1). We say P is positive iff m = 0 for all normal rules (1) in P . For normal programs P , we denote by P + the positive program obtained from P by removing all negative literals from the rule bodies.
The Herbrand universe of a normal program P , denoted HU P , is the set of all terms constructed from constant and function symbols appearing in P . If there is no such constant symbol, then we take an arbitrary constant symbol from . As usual, terms, atoms, literals, rules, programs, etc. are ground iff they do not contain any variables. The Herbrand base of a normal program P , denoted HB P , is the set of all ground atoms that can be constructed from the predicate symbols appearing in P and the ground terms in HU P . A ground instance of a rule r 2 P is obtained from r by uniformly replacing every variable in r by a ground term from HU P . We denote by ground (P ) the set of all ground instances of rules in P . For literals ` = a (resp., ` = :a), we use ::` to denote :a (resp., a), and for sets of literals S, we define ::S = f::` j ` 2 Sg, S+ = fa 2 S j a is an atomg, and S = f:a j :a 2 Sg. We denote by Lit P = HB P [ ::HB P the set of all ground literals with predicate symbols from P and ground terms from HU P . A set of ground literals S Lit P is consistent iff S \ ::S = ;. A (three-valued) interpretation w.r.t. P is any consistent set of ground literals I Lit P . 2.3
Normal BCQs We add negation to BCQs as follows. A normal Boolean conjunctive query (NBCQ) Q is an existentially closed conjunction of atoms and negated atoms 9X p1(X) ^ ^ pm(X) ^ :pm+1(X) ^ ^ :pm+n(X); where m > 1, n > 0, and the variables of the pi’s are among X. We denote by Q+ (resp., Q ) the set of all positive (resp., negative (“:”-free)) atoms of Q. In the sequel, w.l.o.g., BCQs contain no constants. An NBCQ Q is satisfied in an interpretation I Lit P if there is a homomorphism such that (a) 2 I and : (b) 2 I for all a 2 Q+ and b 2 Q . Answers to an NBCQ over a database are then defined as in the case of BCQs. 2.4
Normal TGDs Given a relational schema R, a tuple-generating dependency (TGD) is a first-order formula of the form 8X8Y (X; Y) ! 9Z (X; Z), where (X; Y) and (X; Z) are conjunctions of atoms over R (all these atoms without nulls). Note that TGDs can be reduced to TGDs with only single atoms in their heads. Normal TGDs are informally TGDs that may also contain (default-)negated atoms in their bodies. Given a relational schema R, a normal TGD (NTGD) has the form 8X8Y (X; Y) ! 9Z (X; Z), where (X; Y) is a conjunction of atoms and negated atoms over R, and (X; Z) is a conjunction of atoms over R (all these atoms without nulls). It is also abbreviated as (X; Y) ! 9Z (X; Z). As in the case of standard TGDs, w.l.o.g., (X; Z) is a singleton atom. We denote by head ( ) the atom in the head of , and by body +( ) and body ( ) the sets of all positive and negative (“:”-free) atoms in the body of , respectively.
As for the semantics, a normal TGD is satisfied in a database D for R iff, whenever there exists a homomorphism h for all the variables and constants in the body of that maps (i) all atoms of body +( ) to atoms of D and (ii) no atom of body ( ) to atoms of D (i.e., atoms not in D are false), then there exists an extension h0 of h that maps all atoms of head ( ) to atoms of D.
A normal TGD is guarded iff it contains a positive atom in its body, denoted guard ( ), that contains all universally quantified variables of . W.l.o.g., to simplify such in formal proofs, constants occur only in the guards of (as all the other atoms with constants can be abbreviated by fresh atoms without constants, which can be defined via guarded TGDs). A guarded (normal) Datalog program is a finite set of guarded (N)TGDs.
Given an NTGD = (X; Y) ! 9Z (X; Z), the functional transformation of , denoted f , is the normal rule (X; Y) ! (X; f (X; Y)), where f is a vector of function symbols f ;Z for , one for every variable Z in Z. Given a set of NTGDs, the functional transformation of , denoted f , is obtained from by replacing each TGD in by f . Note that the functional transformation of a guarded Datalog program is a positive program. 2.5
Guarded Chase Forests Let be a guarded Datalog program (without negation) over a relational schema R, let D be a database for R, and let P := D [ f .
The guarded chase forest F (P ) of P is the union of the following forests Fi(P ): We start with a forest F0(P ) that contains, for each fact a in P , a unique node labeled a; there are no other nodes and no edges. Now let i 0. The forest Fi+1(P ) is obtained from Fi(P ) by adding new nodes and edges as follows. Let A be the set of all labels of nodes of Fi(P ). For each node v in Fi(P ) and each rule r 2 ground(P ) such that guard(r) is the label of v and B(r) A, there is a child w of v with label H(r), and the edge from v to w is labeled with r.
Given a graph G, we denote by V (G) the set of nodes of G. We often write v 2 G instead of v 2 V (G). The label of a node v in F (P ) is denoted by label(v). We extend this notation to sets V V (F (P )) by letting label(V ) := Sv2V label(v), and to subforests F by letting label(F ) := label(V (F )). The derivation level of a node v in F (P ), denoted levelP (v), is the smallest integer i 0 such that v 2 Fi(P ). Observe that levelP (v) is in general different from the depth of v in F (P ). We define the derivation level of an atom a in F (P ), denoted by levelP (a), as the minimum of levelP (v) over all nodes v in F (P ) with label a, or as 1 if no such node exists. 2.6
Well-Founded Semantics for Normal Logic Programs
The well-founded semantics [
and WP . A set U HB P is an unfounded set of P relative to I and every r 2 ground (P ) with H(r) = a, either (i) :b 2 I [ ::U for some atom b 2 B+(r), or (ii) b 2 I for some atom b 2 B (r).
There is the greatest unfounded set of P w.r.t. I, denoted UP (I). Intuitively, if I is compatible with P , then all atoms in UP (I) can be safely switched to false and the resulting interpretation is still compatible with P . The greatest unfounded set of a partial interpretation I intuitively collects all those atoms that cannot become true when extending I with further information.
We are now ready to define the two operators TP and WP on consistent I Lit P by putting TP (I) = fH(r) j r 2 ground (P ); B+(r) [ ::B (r) Ig and WP (I) = TP (I) [ ::UP (I). The operator WP is monotonic, and thus has a least fixpoint, denoted lfp(WP ), which is the well-founded semantics of P , denoted WFS (P ) (a three-valued interpretation completable to a two-valued model of P ). A ground atom a 2 HB P is well-founded (resp., unfounded) relative to P , if a (resp., :a) is in lfp(WP ). Intuitively, starting with I = ;, rules are applied to obtain new positive and negated facts (via TP (I) and ::UP (I), respectively). This process is repeated until no longer possible. A literal ` 2 Lit P is a consequence of P under the well-founded semantics iff ` 2 WFS (P ). 3
The well-founded semantics for a guarded normal Datalog program relative to a given database D under the UNA is defined using the well-founded semantics of the logic program obtained from taking the union of the functional transformation of and D. Definition 3. Let R be a relational schema, and be a guarded normal Datalog program. The well-founded model of a database D under , denoted WFS(D; ), is defined as WFS(D [ f ). An NBCQ Q is satisfied over D under w.r.t. the well-founded semantics if WFS(D; ) j= Q.
Example 4. Let be a guarded normal Datalog program such that f has the form: and let D = fR(0; 0; 1); P (0; 0)g. It is easy to see that WFS(D; ) includes the atom R(0; 1; f (0; 0; 1)), as we can apply the first rule in f to derive this atom from the atoms in D. Furthermore, WFS(D; ) includes P (0; 1). To see this slightly less obvious fact, note that there is no rule that can derive an atom of the form R( ; ; 1), where the ’s could be arbitrary constants or nulls. This is due to the fact that any Skolem term of the form f (t1; t2; t3) is by default assumed to be different from 1. Therefore, the only rule instance that could possibly derive Q(1) is R(0; 0; 1) ^ :P (0; 0) ! Q(1), but as P (0; 0) 2 D WFS(D; ), we can conclude that :Q(1) is in WFS(D; ). Now P (0; 1) 2 WFS(D; ) can be derived using a suitable instance of the second rule.
When proving decidability of query answering relative to a Datalog -program, one faces
the problem that query answering has to be performed relative to an infinite model that is
obtained as a result of the chase algorithm. Nevertheless, as demonstrated in [
Characterization via Forward Proofs. To be able to prove the above-mentioned locality
property, we first introduce the notion of a forward proof of an atom. These forward proofs
are subforests of the guarded chase forest of the positive part of a guarded normal Datalog
program that witness the fact that an atom is potentially contained in the well-founded
semantics (an atom without forward proof is certainly false). Forward proofs are instrumental
for proving the locality property as they provide a useful link between the guarded chase
forest of the positive part of the program on the one hand and the well-founded semantics
of the program on the other hand. The characterization of the well-founded semantics for
guarded normal Datalog based on the concept of forward proofs that we are going to use is
essentially the one from [
Let be a guarded normal Datalog program over R, D be a database for R, and P := D [ f . Let F +(P ) be the forest obtained from F (P +) by replacing each edge label, which is a rule r+ 2 ground(P +), by the rule r 2 ground(P ) such that r+ is obtained from r by dropping all negative literals (for simplicity, we assume that r is unique). Let N (F ) be the set of all b 2 HB P such that b 2 B (r) for a rule r that occurs as the label of an edge in F .
The following is a minor modification of the notion of forward proof in [
Example 6. The program P + for P = D [
R(0; 0; 1); P (0; 0); R(X; Y; Z) ^ P (X; Y ) ! P (X; Z); R(X; Y; Z) ! S(X); with D and
chosen as in Example 4 is: The forest F +(P ) up to depth three is shown on the right, where a, b, and c are defined as f (0; 0; 1), f (0; 1; a), and f (0; a; b), respectively. Edge labels are omitted, but they can easily be recovered from the information in Figure 6. For example, the edge from R(0; 0; 1) to R(0; 1; a) is labeled by R(0; 0; 1) ! R(0; 1; f (0; 0; 1)), and the edge from R(0; 1; a) to P (0; a) is labeled by R(0; 1; a) ^ P (0; 1) ^ :Q(a) ! P (0; a). If F is the subtree containing R(0; 0; 1), P (0; 1), and T (0) (the child of P (0; 1)), then N (F ) = fQ(1); S(0)g. So, N (F ) contains all the atoms whose negation is required to fire all the rules in F .
R(0,0,1) P(0,0) R(0,1,a) P(0,1) R(0,a,b) P(0,a) R(0,b,c) P(0,b)
T(0)
Q(1) S(0) T(0)
Q(a) S(0) T(0)
Q(b) S(0) T(0)
There is exactly one inclusion-minimal forward proof of R(0; b; c) from P , namely the subtree of F +(P ) induced by the nodes labeled R(0; 0; 1), R(0; 1; a), R(0; a; b), and R(0; b; c). Note that N ( ) = ;.
The atom P (0; a) has exactly one inclusion-minimal forward proof from P : the subforest 0 induced by the nodes labeled R(0; 0; 1), R(0; 1; a), P (0; 0), P (0; 1), and P (0; a). Here, N ( 0) = fQ(1); Q(a)g. But note that there are infinitely many inclusion-minimal forward proofs of S(0) from P , each corresponding to a node in F +(P ) labeled with S(0).
We need the following operator from [
Definition 7 (WcP ). We define an operator WcP on P(Lit P ) as follows. For every I and every a 2 HB P : Lit P – a 2 WcP (I) if there is a forward proof of a from P with ::N ( ) I, and – :a 2 WcP (I) if for all forward proofs of a from P there is a b 2 N ( ) with b 2 I. WcP; := WcP (WcP; 1) if is a successor ordinal, and WcP; := S < ordinal. Now:
It is not hard to see that WcP is monotone, and therefore has a least fixpoint. Recall that this least fixpoint is defined as the union of the fixpoint stages WcP0 ; WcP1 ; : : : , where WcP;0 := ;,
Theorem 8 ([
Example 9. Let us revisit Example 6. Define t0 := 0, t1 := 1, and ti+2 := f (0; ti; ti+1). Then, we have WcP;1 = fR(0; ti; ti+1) j i 0g [ fP (0; 0)g [ f:a j a 2 HB P ; a 2= label(F +(P ))g: It is not hard to see that for every integer i 1, WcP;2i = WcP;1 [ fP (0; tj ) j 0 j < ig [ f:Q(tj ) j 0 j ig and WcP;2i+1 = WcP;1 [ fP (0; tj ) j 0 j ig [ f:Q(tj ) j 0 j ig. Therefore,
WcP;!+2 = WcP;1 [ fP (0; tj) j j 0g [ f:Q(tj) j j 0g [ f:S(0); T (0)g; and WcP;!+3 = WcP;!+2, hence WFS(P ) = WcP;!+2.
This demonstrates that the computation of the least fixpoint of WcP does in general not terminate after !-many steps. The same is true if we compute WFS(P ) as least fixpoint of WP : spelling out the definitions, one can check that WP!(;) = WcP;!.
Locality. After having introduced the characterization of the well-founded semantics in terms of forward proofs, we are now ready to prove the locality property of the well-founded semantics that we discussed at the beginning of this section.
Throughout this section, we fix a finite set of guarded NTGDs over a relational schema R, and a database D for R. Let P := D [ f .
The (P -)type of an atom a 2 HB P is the pair typeP (a) := (a; S), where S consists of all literals ` 2 WFS(P ) with dom(`) dom(a). If we speak of a P -type without mentioning the atom, we mean a P -type of some atom.
Let I; I0 Lit P and X dom(I) [ dom(I0). An X-isomorphism from I to I0 is a bijective mapping f from dom(I) to dom(I0) such that f (I) = I0, and for all x 2 X, (1) x 2 dom(I) if and only if x 2 dom(I0), and (2) if x 2 dom(I), then f (x) = x. If there is an Xisomorphism from I to I0, then I and I0 are X-isomorphic, denoted I =X I0. Given two P types (a; S) and (a0; S0), an X-isomorphism from (a; S) to (a0; S0) is an X-isomorphism f from fag to fa0g with f (S) = S0. As for sets of literals, (a; S) and (a0; S0) are X-isomorphic, denoted (a; S) =X (a0; S0), if there is an X-isomorphism from (a; S) to (a0; S0).
Let F (P ) be the subforest of F +(P ) induced by all the nodes in F +(P ) that are goal nodes of forward proofs from P with ::N ( ) WFS(P ). Note that F (P ) contains exactly the nodes that correspond to the atoms in WFS(P ). The following lemma demonstrates that the truth of any atom below some node v 2 F (P ) depends only on the type of label(v), the labels of the tree T generated by v, and all negative literals whose arguments occur in the labels of T .
Lemma 10. Let v 2 F (P ) with typeP (label(v)) = (a; S), let T be the subtree of F +(P ) rooted at v, and let I be the set of all literals ` 2 Lit P such that either ` 2 S, or ` is positive and occurs in T , or ` is negative and dom(`) dom(label(T )). Then, for all atoms b 2 label(T ), we have: 1. If there is a forward proof of b from P with ::N ( ) X WFS(P ), then there exists a forward proof 0 of b from S+ [ f with ::N ( 0) X \ I and with the property that label( 0) S [ label(T ). 2. If there exists a forward proof 0 of b from S+ [ f , then 0 can be extended to a forward proof of b from P with ::N ( ) n ::N ( 0) WFS(P ).
We are now able to formulate and prove the locality property of the well-founded semantics that is crucial for our decidability result.
Lemma 11. Let v1; v2 2 F (P ) be two nodes with the types typeP (label(vi)) = (ai; Si) for i 2 f1; 2g. Let Ti be the subtree of F +(P ) rooted at vi, and let Ii be the set of all literals ` 2 Lit P such that either ` 2 Si, or ` is positive and occurs in Ti, or ` is negative and dom(`) dom(label(Ti)). If f is an X-isomorphism from typeP (a1) to typeP (a2), then there is an X-isomorphism from WFS(P ) \ I1 to WFS(P ) \ I2 that extends f .
The locality property from the previous lemma is the key for obtaining the following
bound on the possible matches of a normal Boolean conjunctive query. Its proof is a
generalization of the proof of Lemma 4 in [
Proposition 12. Let R be a relational schema R, and := 2 jRj (2w)w 2jRj (2w)w , where w is the maximum arity of a predicate in R. Let D be a database for R, be a set of guarded NTGDs over R, and Q be an NBCQ over R with n literals. If WFS(D [ f ) j= Q, then there is a homomorphism of Q into WFS(D [ f ) such that: 1. For all a 2 Q+, (a) has depth at most n in F (P ). 2. For all a 2 Q , (a) does not occur in F +(P ), or (a) has depth n in F +(P ). 4
This section presents our complexity bounds for evaluating NBCQs in well-founded models
under guarded normal Datalog programs. We start by describing the most important
building block—an alternating algorithm, called WCHECK, that decides whether a ground atom
belongs to the well-founded model of a database under a guarded normal Datalog program.
Due to space limitations, we only give a high-level overview of WCHECK, explaining the
underlying ideas as well as the problems that we need to tackle. For a detailed description
and proofs, we refer the reader to [
WCHECK’s goal is to decide whether a ground atom belongs to the well-founded model of some database under a guarded normal Datalog program. More precisely, its input consists of a database D, a guarded normal Datalog program , and a ground atom a, and its task is to decide whether a 2 WFS(P ), where P = D [ f .
For the case that is positive (i.e., contains only NTGDs without negated atoms in
their bodies), the task of deciding whether a belongs to WFS(P ) is well-understood [
Although the method for checking membership of ground atoms in well-founded models
over positive guarded normal Datalog programs described above does not generalize to
arbitrary guarded normal Datalog programs, it turns out that a different one, namely the
ACHECK algorithm in [
WCHECK is based on the idea that, if a ground atom a belongs to the well-founded model
W of a database D and a guarded normal Datalog program , then the forest F +(D [ f )
contains a path from some root node to a node labeled a such that all “side literals” (i.e.,
nonguard atoms and negated atoms in the bodies of rules applied along the path) belong to W
(this is actually true also for non-ground atoms). For example, in the case of D and from
Example 4, the atom T (0) belongs to W , and indeed F +(D [ f ) contains a path from the
root R(0; 0; 1) to T (0) whose side literals P (0; 1), :Q(f (0; 0; 1)), and :S(0) belong to W .
The idea is quite similar to ACHECK’s central idea. The only difference is that in the case of
ACHECK, is a positive guarded normal Datalog program, W is the result of the chase
of D and , and side literals are replaced by “side atoms” [
To decide whether a path from the root of F +(D [ f ) to a with the desired properties exists, WCHECK successively guesses atoms a0; a1; a2; : : : , where a0 is the label of a root of F +(D [ f ), and each ai+1 is the label of a child of (the node labeled) ai. The idea here is to guess a path from a0 to a. Of course, we also need to verify that all the side literals on such a path belong to W . Therefore, along with each ai, WCHECK guesses a set Si of literals in W all of whose arguments appear in ai and which agree with Si 1 on the literals whose arguments appear in ai 1, and an ordering i of the literals in Si (more precisely, a total preorder that is a linear order on the atoms). The idea is that Si contains (at least) all the side literals of rules applied on the path from ai to a that contain only arguments from ai (this is enforced by checking that the rule generating ai+1 has all its side-literals in Si), and i is the order of deriving the atoms in Si. For example, if D and are as in Example 4, a is the atom T (0), and WCHECK guesses a0 = R(0; 0; 1), a1 = R(0; 1; f (0; 0; 1)), a2 = P (0; f (0; 0; 1)), and a3 = T (0), then good choices for the sets Si would be S0 = fP (0; 1); :S(0)g, S1 = S0 [ f:Q(f (0; 0; 1))g, S2 = f:Q(f (0; 0; 1)); :S(0)g, and S3 = f:S(0)g
What remains is to check that all the literals in Si belong to W . To this end, WCHECK launches subcomputations, one for each literal in an Si. The subcomputations for positive literals b 2 Si, where i is assumed to be minimal, are similar to the main computation described above. For i > 0 (for 0, it is basically the same as above), the basic idea is to find a path from ai to b such that all side literals along the path belong to W (where literals in Si 1 and literals in Si that are i-smaller than b may be assumed to belong to W ). This is justified because b is in Si n Si 1, and as such it contains at least one element that was created in ai and must therefore occur in the subtree rooted at ai. The case of negative literals :b 2 Si is not so clear. The main idea is to check that every path from ai to a node labeled b contains either a positive side literal c with :c 2 W , or a negative side literal :c with c 2 W (where literals in Si 1 and literals in Si that are smaller or equal to :b with respect to i may be assumed to belong to W ). In our example above, WCHECK would find out that the only path (and thus all paths) from a1 = R(0; 1; f (0; 0; 1)) to Q(f (0; 0; 1)) in F +(D [ f ) contains the side literal :P (0; 1), and since it knows that P (0; 1) 2 W (since it belongs to S0), it would conclude that :Q(f (0; 0; 1)) 2 S1 belongs to W . It is not obvious, though, that this test is enough to establish that :b belongs to W . Its proof requires the machinery and results from the locality part of Section 3.
The above-sketched WCHECK algorithm can be implemented in such a way that it
uses space at most jDjjRj 2O(w) , where R is the schema and w is the maximum arity of a
predicate in R. It can furthermore be shown that WCHECK correctly decides whether a 2
WFS(D; ). This yields the upper bounds of the following theorem; the lower bounds follow
from the corresponding lower bounds for answering BCQs under guarded Datalog [
The complexity bounds for deciding membership of ground atoms can be extended to deciding membership of arbitrary literals. For positive literals a, the idea is to guess a path to a, using WCHECK to verify the literals along the path. For negative literals :a, we have to check that every path to a contains a side-literal whose complement belongs to the wellfounded model; WCHECK is again used to verify literals along to the path.
These complexity bounds and Proposition 12 form the key for proving our main result, Theorem 14, on answering NBCQs in well-founded models under guarded normal Datalog . Theorem 14. Given a database D for a schema R, a guarded normal Datalog program over R, and an NBCQ Q over R, the problem of deciding WFS(D; ) j= Q is: 1. 2-EXPTIME-complete in general. 2. EXPTIME-complete in case w is bounded. 3. in PTIME in case jRj, the maximum arity w of a predicate symbol in R, and the number of literals in Q are bounded; there are cases where the problem is PTIME-complete. 5
We have introduced the standard well-founded semantics (WFS) for normal Datalog
programs under the unique name assumption (UNA). We have shown that for guarded normal
Datalog under the standard WFS, answering normal Boolean conjunctive queries is
decidable. Furthermore, we have shown that this problem is complete for PTIME in the data
complexity, and that it is complete for 2-EXPTIME in the combined complexity in general
and complete for EXPTIME in the combined complexity in the case where the arities of all
predicates are bounded by a constant. A topic of future research is to explore how to add
negative constraints and equality-generating dependencies (EGDs), similarly to [