Not too Big, Not too Small... Complexities of Fixed-Domain Reasoning in First-Order and Description Logics? Sebastian Rudolph and Lukas Schweizer firstname.lastname@tu-dresden.de Technische Universität Dresden, Computational Logic Group Abstract. We consider reasoning problems in description logics and variants of first-order logic under the fixed-domain semantics, where the model size is fi- nite and explicitly given. It follows from previous results that standard reasoning is NP-complete for a very wide range of logics, if the domain size is given in unary encoding. In this paper, we complete the complexity overview for unary encoding and investigate the effects of binary encoding with partially surprising results. Most notably, fixed-domain standard reasoning becomes NE XP T IME for the rather low-level description logics ELI and ELF (as opposed to E XP T IME when no domain size is given). On the other hand, fixed-domain reasoning re- mains NE XP T IME even for first-order logic, which is undecidable under the un- constrained semantics. For less expressive logics, we establish a generic criterion ensuring NP-completeness of fixed-domain reasoning. Amongst other logics, this criterion captures all the tractable profiles of OWL 2. 1 Introduction Description logics (DLs, [2, 14]) and other fragments of first-order logic are popular knowledge representation (KR) formalisms. Traditionally, the semantics underlying these formalisms do not constrain the number of elements of the described domain of interest; classical KR even admits models of infinite size. In many realistic knowl- edge representation scenarios, however, it is known that the domain must be finite, or even a bound on its size is given. In such scenarios, the classical semantics allowing for models of arbitrary (even infinite) size does not adequately reflect the reasoning requirements. Consequently, KR research has recently started to consider alternative semantics, leading to numerous novel (un)decidability and complexity results. The finite model semantics, inspired by database theory, requires models to be finite (but of arbitrary size). Finite satisfiability checking and finite query entailment have been considered for a variety of description logics [11, 5, 13, 15]. Still, in some situa- tions just requiring finiteness of the domain is not restrictive enough; sometimes the complete set of domain elements (or at least their precise number) are known, leading to the notion of the fixed-domain semantics [8]. First complexity investigations have shown that standard reasoning tasks are NP-complete for a wide range of DLs, when ? A version of this paper has been accepted for publication at EPIA (2017). the elements of the fixed domain are explicitly enumerated. These results directly carry over to the case where only the number of domain elements is provided but this number is given in unary encoding. Previous work has left open (or has been too unspecific on) important questions re- garding fixed-domain reasoning. First, it was not explicitly investigated, if and how the complexity results would be affected if the domain size would be considered as a fixed parameter rather than a variable part of the input. Second, reasoning complexities of (fragments of) first-order logic (which are undecidable under classical and finite-model semantics but become decidable when fixing the domain) have not been investigated thoroughly. Third, the effect of representing the size of the domain in binary encoding has not been considered at all. In this paper, we clarify the complexity landscape for fixed-domain standard reasoning in first-order logic and description logics by making the following contributions. – We show that for unrestricted first-order logic, standard reasoning is NE XP T IME, no matter if the domain size is a fixed parameter or given in unary or binary as part of the input. For fixed size or unary encoding, the complexity drops to PS PACE when bounding the predicate arity, and to NP when the number of variables is bounded. – We show that for the binary encoding, the complexity remains NE XP T IME, even when the logic is drastically restricted. In particular, we show corresponding hard- ness results for ELI and ELF terminologies. – Finally, we establish NP-completeness for the binary encoding case for a wide range of lightweight logics by introducing a model-theoretic property shared by these logics and showing that it warrants NP-membership. 2 Preliminaries 2.1 KR Formalisms We assume the reader to be familiar with the basics of DLs [2, 14], as well as with the DL SROIQ [9], of which we briefly recap some fragments we will use throughout this paper. EL / ELI / ELF Terminologies EL terminologies are knowledge bases with only axioms of the form C v D, where C, D are concept expressions built from concept and role names using only top, conjunction, and existential quantification. We consider two extensions: ELI terminologies additionally allow the usage of role inverses, while ELF terminologies admit role functionality axioms of the shape > v 61 r.C. DLmin Knowledge Bases With DLmin , we refer to a minimalistic description logic that merely allows TBox axioms of the form A v ¬B, with A, B ∈ NC . Moreover, only atomic assertions of the form A(a) are admitted. It is immediate that (finite) satisfiabil- ity checking in DLmin is in AC0 . First-Order Logic We assume the reader to be familiar with syntax and semantics of first-order predicate logic (FOL). By default, we assume that the only functions oc- curring are of arity zero (i.e., constants). We use FOL= to denote FOL with equality. By bounded-arity FOL(=) we denote FOL(=) using only predicates of arity smaller or equal to a given bound. By bounded-variable FOL(=) we denote FOL(=) using only a bounded number of variables. For uniformity, we use the typical DL notation also for first-order interpretations and we refer to FOL(=) sentences as (FOL(=) ) axioms and to FOL(=) as (FOL(=) ) knowledge bases. We recall that virtually all mainstream DLs (including SROIQ) can be expressed in bounded-arity FOL= . We also recall that Datalog denotes the function-free first-order Horn clauses. 3 Fixed-Domain Semantics In this paper, we investigate the effects of fixing the domain size of models. Given some s ∈ N, we say a knowledge base K is s-satisfiable, if it has a model I = (∆I , ·I ) with |∆I | = s (referred to as an s-model) and an axiom ϕ is s-entailed by K (written: K |=s ϕ) if every s-model of K is a model of ϕ. We define s-subsumption accordingly. Depending on how we treat the size parameter s, we distinguish three versions of the fixed-domain entailment decision problem (where, the function || · || determines the size of a knowledge base or axiom according to some usual encoding): – assuming s fixed, the input is (K, ϕ); the problem size is ||K||+||ϕ|| – the input is (K, ϕ, s) with s in unary; the problem size is ||K||+||ϕ||+s – the input is (K, ϕ, s) with s in binary; the problem size is ||K||+||ϕ||+dlog2 se In all cases, the output is “yes” if K |=s ϕ and “no” otherwise. We define the three versions of the fixed-domain satisfiability problem accordingly. 4 Fixed and Unary Encoding 4.1 Variants of First-Order Logic We first consider the case of unrestricted first-order logic, rectifying an incorrect re- sult from the literature. Without giving a proof, Gaggl et al. [8] claim that this prob- lem is PS PACE-complete, sketching an argument based on the assumption that any FOL model with polynomially many domain elements can be represented in polyno- mial space, which, however, only holds when the maximum predicate arity is bounded (see our results below). In fact, we can show that even for domain size 2, the problem is NE XP T IME-hard (even when no constants are used). We use a reduction from the TILING-problem, as it can be found in [12], which is known to be NE XP T IME-hard. Definition 1 (n×n Tiling Problem). Given a set of square tile types T = {t0 , . . . , tk }, together with two relations H, V ⊆ T × T (horizontal and vertical compatibility, respectively), as well as an integer n in binary. An n × n tiling is a function f : {1, . . . , n}×{1, . . . , n} 7→ T such that (a) f (1, 1) = t0 , and (b) for all i, j (f (i, j), f (i+ 1, j)) ∈ H, and (f (i, j), f (i, j + 1)) ∈ V . TILING is the problem of deciding, given T, H, V , and n, whether an n × n tiling exists. We refer to given T ,H,V , and n as tiling system T = (T, H, V, n). Theorem 1. The 2-satisfiability problem for constant-free FOL is NE XP T IME-hard. Proof. We provide a reduction from TILING. Let n be the size of the grid. W.l.o.g. we assume n = 2m . We now provide a FOL knowledge base (of size polynomial in m) which is satisfiable iff a tiling exists. In the following, ~x stands for the sequence x0 , . . . , xm−1 of variables (likewise ~y and ~z). ∃x, y.1(x) ∧ 0(y) ∀x.1(x) ↔ ¬0(x) (1) ∀x, y.same(x, y) ↔ (1(x) ↔ 1(y)) (2) ^ ^ ∀~ x, ~ y .flipi (~ y) ↔ x, ~ (1(xj ) ∧ 0(yj )) ∧ 0(xi ) ∧ 1(yi ) ∧ same(xj , yj ) (3) j∈{0...i−1} j∈{i+1...m−1} _ ∀~ x, ~ y .next(~ y) ↔ x, ~ flipi (~ x, ~ y) (4) i∈{0...m−1} ∀~ x, ~ y .¬(ti (~ y ) ∧ tj (~ x, ~ x, ~ y )) (5) ^ ∀~ x, ~ y. (0(xi ) ∧ 0(yi )) → t0 (~ x, ~ y) (6) i∈{0...m−1} _ _ ∀~ x, ~ y , ~z.next(~ y) → x, ~ x, ~z) ∧ tj (~ ti (~ y , ~z) ∧ x) ∧ tj (~z, ~ ti (~z, ~ y) (7) (ti ,tj )∈H (ti ,tj )∈V With this knowledge base and a domain of size two, we use the two elements as 0 and 1 to encode the coordinates in the grid (0 . . . 2m − 1) in binary, using m positions in the predicate for each coordinate. With this encoding, the next predicate is axiomatized to contain any pair of consecutive m-bit numbers. Then the ti predicates indicate the coordinate pairs of grid positions where the tile ti is positioned. t u A matching upper bound will be provided through Theorem 4. The proof of the preceding theorem suggests that an unbounded predicate arity is essential for the result. Indeed, when bounding the maximal arity, the complexity can be shown to be PS PACE- complete. Theorem 2. The fixed-domain satisfiability problem for bounded-arity FOL(=) is PS PACE-complete when the domain size is fixed or given unary. Proof. We show PS PACE-hardness of FOL satisfiability for domain size 2 by providing a reduction from the validity problem of quantified Boolean formulae (QBFs). We recap that for any QBF, it is possible to construct in polynomial time an equivalent QBF that has the specific shape ψ = Q1 x1 Q2 x2 . . . Qn xn ϕ with Q1 , . . . Qn ∈ {∃, ∀} and ϕ being a propositional formula over the propositional variables x1 , . . . , xn . Let the first- order sentence ψ 0 be obtained from ψ by replacing every occurrence of a propositional variable xi by true(xi ) (thus reinterpreting the propositional variables as first-order variables and introducing true as the only unary predicate). It is now easy to see that ψ is true iff ψ 0 ∧ ∃x.true(x) ∧ ∃x.¬true(x) has a model with two elements. We show PS PACE membership of FOL(=) satisfiability checking for domain size given in unary encoding by providing a PS PACE decision procedure for a given K and domain size s. Let k = ||K|| and ` = k + s. Let a be the upper bound on the arity. There can be at most k predicates, hence the size needed to represent a model is upper- bounded by k · sa ≤ ` · `a , i.e., polynomial. Then we guess a polynomial size model representation and verify it in PS PACE [17]. This gives an NPS PACE algorithm which by Savitch’s theorem [16] can be turned into a PS PACE one. t u Again, inspecting the previous proof, it seems to be essential that the number of used variables is unbounded. The subsequent theorem confirms that bounding the number of variables will lead to NP-membership. Theorem 3. The fixed-domain satisfiability problem for bounded-variable FOL= is in NP when the domain size is given in unary encoding. Proof. Let v be the upper bound on the number of variables. Let K be a FOL knowledge base with at most v variables, let s be the prescribed domain size and let ` = ||K|| + s. V a nondeterministic polytime procedure for checking s-satisfiability of We now describe K. Let ϕ = α∈K α and let I be a model of ϕ (and, hence, of K) with |∆I | = s. We guess cI for every free constant c occurring in K. We also guess for every subformula ψ of ϕ the set Zψ of variable assignments ν : freevars(ϕ) → ∆I for which I, ν |= ψ. We determine an upper bound for the size of the guessed information: ϕ has not more than 2` subformulae each of which has maximally v free variables, hence the size to store all Zψ is bounded by 2` · sv and hence by 2` · `v , i.e., polynomial in the input. Verifying that the guessed information indeed satisfies the abovementioned property requires four checks: first, Zϕ must contain the empty function. Second, every Zψ must be compatible with the variable assignments of ψ’s subformulae in the following way (where δ ranges over ∆I ): Z¬ψ = (∆I )freevars(ψ) \ Zψ Zψ1 ∧ψ2 = {ν ∈ (∆I )freevars(ψ1 ∧ψ2 ) | Zψ1 ⊆ν and Zψ2 ⊆ν} Zψ1 ∨ψ2 = {ν ∈ (∆I )freevars(ψ1 ∨ψ2 ) | Zψ1 ⊆ν or Zψ2 ⊆ν} Z∃x.ψ = {ν ∈ (∆I )freevars(∃x.ψ) | ∃δ : ν ∪ {(x, δ)} ∈ Zψ } Z∀x.ψ = {ν ∈ (∆I )freevars(∀x.ψ) | ∀δ : ν ∪ {(x, δ)} ∈ Zψ } . Third, for any atomic subformula ψ which is an equality atom t1 = t2 , we need to check that ν ∈ Zψ exactly if ν (t1 ) = ν (t2 ) where, given a ν, we let ν ∗ denote the extension ∗ ∗ of ν to arbitrary terms, mapping constants c to cI (as guessed before). Fourth, for any two atomic subformulae ψ1 = p(t1 , . . . , tk ) and ψ2 = p(t01 , . . . , t0k ), referring to the same predicate p, we need to check that they do not contradict each other w.r.t. any k-tuple being or not being in pI . This is checked by verifying if {(ν ∗ (t1 ), . . . , ν ∗ (tk ) | ν ∈ Zψ1 )} ∩ {(ν ∗ (t01 ), . . . , ν ∗ (t0k ) | ν ∈ (∆I )freevars(ψ) \ Zψ2 )} = ∅, with ν ∗ defined as before. Note that the sets in this condition do only have polynomially many elements. All these checks can be done in polynomial time. Hence we obtain an NP upper bound for checking satisfiability. t u 4.2 Upper and Lower Bounds for DLs We recall from Gaggl et al. [8] that fixed-domain standard reasoning in SROIQ with unary encoding is in NP. Note that this result is not subsumed by Theorem 3 since encoding number restrictions may require an unbounded number of variables. For one lower bound, we recall that 3-satisfiability is already NP-hard for DLmin [8], a very minimalistic DL that is subsumed by all tractable profiles of OWL. To also provide a lower bound for logics without ABox, we add a hardness result for terminologies. Proposition 1. Deciding 3-subsumption in EL terminologies is CO NP-hard. Proof. We provide a reduction from the 3-colorability problem to non-3-subsumption. For a graph (V, E) with V = {v1 , . . . , vn }, we introduce a concept name Avi for every vertex and one distinguished concept name Clash. Then we let the terminology K consist of the axioms Avi u Avj v Clash for every {vi , vj } ∈ E. Then the graph is not 3-colorable iff K |=3 ∃r.Av1 u ... u ∃r.Avn v ∃r.Clash. t u 5 Binary Encoding 5.1 NE XP T IME Upper Bound for FOL Theorem 4. The fixed-domain satisfiability problem for FOL= with the domain size given in binary is in NE XP T IME. Proof. Let K be a FOL knowledge base, s the prescribed domain size and let ` = ||K|| + dlog2 se. We now describe a V nondeterministic exponential time procedure to check s-satisfiability of K. Let ϕ = α∈K α. We guess a model I of ϕ (and, hence, of K) with |∆I | = s and for every subformula ψ of ϕ we guess the set Zψ of variable assignments ν : freevars(ϕ) → ∆I for which I, ν |= ψ. We determine an upper bound for the size of the guessed information: ϕ can contain at most ` different predicates and ` is also an upper bound for the arity of the predicates 2 used in ϕ. Therefore, the size to store I is bounded by `·s` and hence by `·(2` )` = `·2` . ϕ has not more than 2` subformulae each of which has maximally ` free variables, hence the size to store all Zψ is bounded by 2` · s` and hence by 2` · (2` )` = 2` · 2 2` . Verifying the claimed properties of I and all Zψ then can be done in polynomial time w.r.t. the exponential size input. Hence we obtain a NE XP T IME upper bound for checking satisfiability. t u This result subsumes NE XP T IME membership of fixed-domain satisfiability in all main- stream description logics. Also, by reducibility to FOL satisfiability checking, it follows that axiom entailment, conjunctive query entailment and even entailment of arbitrary Datalog queries (subsuming all kinds of navigational queries) is in CO -NE XP T IME. 5.2 NE XP T IME Lower Bound for ELI and ELF We show CO -NE XP T IME hardness for subsumption in ELI and ELF terminologies under the fixed-domain semantics in binary encoding. Note that for both logics, the problem is E XP T IME-complete under the classical or finite-model semantics [10]. We show that constraining the domain size allows for encoding tiling problems. Similar constructions for much more expressive DLs have been described before [4, 18]. Reducing Tiling Problems to ELI Subsumption Given T = (T, H, V, n) (cf. Sec- tion 4.1), we construct an ELI terminology KT such that every model of KT not sat- isfying a certain subsumption (called countermodel) represents a tiling. For simplicity, we assume n = 2m . The countermodels we axiomatize shall consist of two types of do- main elements: elements corresponding to grid positions and elements representing tile types. The former will be endowed with their x- and y-coordinates in binary representa- tion, using concept names Xiz , Yiz , with (0 ≤ i < m) and z ∈ {0, 1} to encode the each of the m bits of each coordinate. By means of the following axioms, we axiomatize the n × n grid: ∃h − .(Xj0 u Xi0 ) v Xi0 ∃h − .(Xj0 u Xi1 ) v Xi1 (0 ≤ j < i) (8) − ∃h .((X01 u . . . u Xi−1 1 ) u Xi0 ) v Xi1 (9) ∃h − .((X01 u . . . u Xi−1 1 ) u Xi1 ) v Xi0 (10) ∃v − .Xiz v Xiz Xiz v Grid Xi0 v ∃h.Grid (11) Xi0 u Xi1 v C⊥ ∃h.C⊥ v C⊥ (12) 0 0 Origin v X0 u . . . u Xm−1 u Y00 u . . . u Ym−1 0 (13) with 0 ≤ i < m and z ∈ {0, 1}. Likewise, we let KT contain axioms obtained from axioms (8–12) where the Xiz are replaced by Yiz and the roles v and h are swapped. Axioms in (8) ensure that, the value of the ith bit of the x-coordinate does not change when going in horizontal direction, if some preceding bits are set to low. Correspond- ingly, Axioms (9–10) ensure, that the ith bit changes its value, if all preceding bits are set to high. The axioms in (11) enforce that there is an h-successor, as long as one of the Xiz bits is still set to low, thus stopping after 2m consecutive h-successors. Natu- rally, a bit can only be set to one value which is reflected in the axioms in (12).1 Then, instances of the first axiom in (11) merely ensure that Xiz bit values remain unchanged when moving vertically. Finally, in (13) we use Origin to refer to the grid origin. We now turn to the domain elements representing the tile types. We will make sure that every countermodel contains one element per tile type and that every grid element is associated with one tile type via the tiledBy role. Regarding the tiling conditions in T, H, V , the following axioms are used: Tilei v Tile (0 ≤ i ≤ k) Tilei u Tilej v C⊥ (0 ≤ i < j ≤ k) (14) Origin v ∃tiledBy.Tile0 (15) Grid v ∃tiledBy.Tile Grid u Tile v C⊥ (16) Origin v ∃req.Tile1 u . . . u ∃req.Tilek (17) ∃tiledBy.Tilei u ∃h.∃tiledBy.Tilej v C⊥ (18) ∃tiledBy.Tilei u ∃v .∃tiledBy.Tilej v C⊥ (19) where for each (ti , tj ) 6∈ H and (ti , tj ) 6∈ V we find an instance of (18) or (19), respectively. Axiom (15) encodes the initial tiling condition, whereas (17) enforces the existence of Tilei instances whenever Origin is nonempty. 1 Disjointness (A v ¬B) of concepts A, B are modeled in ELI as A u B v C⊥ , where C⊥ is a freshly introduced concept name that acts as the bottom concept in countermodels [1]. Lemma 1. For given T = (T, H, V, n), let KT be the ELI terminology described above, and let s = n2 + k + 1. Then KT 6|=s Origin v C⊥ iff T has a tiling. Proof. (⇒) Recall that n = 2m . Let I = (∆I , ·I ), with |∆I | = 22m + k + 1 = s, be the countermodel for the subsumption Origin v C⊥ , i.e., there is a δ ∈ ∆I , such that δ ∈ Origin I , but δ 6∈ C⊥ I . Moreover, since I |=s KT , we know that there are elements τ0 , . . . , τk ∈ ∆I , with τi ∈ Tilei I , and in particular (δ, τ0 ) ∈ tiledBy I satisfying the initial tiling condition. Now given x, y ∈ {1, . . . , 2m }, let x0 x2 . . . xm−1 and y0 y2 . . . ym−1 be the binary representations of x − 1 and y − 1, respectively. Then we let Cx,y denote the shorthand notation for the concept: Cx,y ≡ X0xi u . . . u Xm−1 xi u yi yi I Y0 u . . . u Ym−1 . Axiom (13) then ensures δ ∈ C1,1 . It follows from Axiom (11) that, (δ, δ 0 ) ∈ v I , (δ, δ 00 ) ∈ h I for some δ 0 , δ 00 ∈ ∆I , where δ 0 ∈ C1,2 I and δ 00 ∈ C2,1 I 0 0 I 00 00 I due to axioms (8–10). Further, there must be (δ , γ ) ∈ h and (δ , γ ) ∈ v , with γ 0 , γ 00 ∈ C2,2 I . In the same vein, by induction on x and y it follows that, for each possible I I (x, y), |Cx,y | ≥ 1, and for every x > 1, at least one β ∈ Cx,y has an incoming h-role 0 I I from some β ∈ Cx−1,y , just as for every y > 1, one β ∈ Cx,y has an incoming v-role 0 I from some β ∈ Cx,y−1 . Note that no element on the binary tree thus created can be in I Cx,y and CxI0 ,y0 at the same time for (x, y) 6= (x0 , y 0 ) since any γ ∈ (Cx,y u Cx0 ,y0 )I I I would also satisfy P γ ∈ C⊥ leading to δ ∈ C⊥ , contradicting our assumption. 0 I I Let now s = x,y |Cx,y |, and assume |Cx,y | > 1, i.e., there are several elements carrying the same coordinate. Recall that k + 1 distinct domain elements are required for the tiles, but then s−(k +1) = 22m < s0 . This contradicts the assumption, therefore I |Cx,y | = 1 for all x and y, effectively leading to all elements of Grid forming an n × n grid with h and v encoding horizontal and vertical neighbourhood, respectively. Axioms (16) and (18–19) then ensure that the assignment of tiles to grid positions satisfies the horizontal and vertical compatibility constraints of H and V , respectively. (⇐) By the arguments above it is immediate that from every correct tiling, a coun- termodel for the subsumption Origin v C⊥ can be extracted. t u We want to emphasize that the imposed domain size is crucial for a) enforcing a grid of exponential size, and b) for exploiting the non-deterministic choice in tile assignments. Theorem 5. Subsumption in ELI under the fixed-domain semantics with binary en- coding is CO -NE XP T IME-hard. Proof. Note that for a given T = (T, H, V, 2m ), the corresponding ELI terminology KT is of polynomial size in m. From Lemma 1 it then follows that, subsumption in ELI is CO -NE XP T IME-hard. t u We finish the section by showing the same complexity for ELF by virtue of a small adaptation of the above argument. Theorem 6. Subsumption in ELF under the fixed-domain semantics with binary en- coding is CO -NE XP T IME-hard. Proof. We reuse the construction made for ELI with the following modification: for r ∈ {h, v} we add the axioms > v 61 r.> and we turn every axiom of the shape ∃r− .C1 v C2 into the axiom C1 v ∃r.C2 . It can be readily checked that the result- ing knowledge base is an ELF terminology. Moreover, the countermodels obtained for ELI satisfy the functionality restriction imposed. Finally, in the presence of function- ality of r, C1 v ∃r.C2 entails ∃r− .C1 v C2 , hence all the arguments in Lemma 1 carry over to this case. t u 5.3 Logics Below NE XP T IME We recall that even for a domain of fixed size and not part of the input, standard rea- soning is already NP-hard for DLmin knowledge bases and EL terminologies (cf. Sec- tion 4.1, Theorem 1). Obviously these hardness results carry over to the unary and binary encoding case and to any logic subsuming any of the two. We now show that a generic property that is shared by many tractable DLs ensures NP-membership of standard reasoning tasks with domain size given in binary. We start with some model- theoretic considerations. Definition 2. We call a model nontrivial if its domain size is larger than 1. A knowledge base is called nontrivially satisfiable, if it has a nontrivial model. A logic L has the polynomial nontrivial model property if there is a polynomial function p : N → N such that every nontrivially satisfiable L knowledge base of size k has a nontrivial model with at most p(k) elements. This property has been shown to hold for a variety of prominent tractable logics. Among those, the recently introduced role-safety-acyclic Horn-SHOIQ [6] is rather general and subsumes the tractable profiles OWL QL and OWL RL of the Web On- tology Language. Another logic satisfying this property is EL++ , even the version extended by reflexive roles and range restrictions [3, 1] subsuming the third tractable OWL profile OWL EL. Finally, the property holds trivially for Datalog, since there is always a model containing only as many individuals as there are constants. In the following, we will introduce two kinds of model transformations and state some logics for which modelhood is preserved under these operations. Definition 3. Let I = (∆I , ·I ) and J = (∆J , ·J ) be interpretations. The product interpretation of I and J , denoted I × J is the interpretation K with ∆K = ∆I × ∆I , aK = (aI , aJ ) for all a ∈ NI , AK = AI × AK for all A ∈ NC , and rK = {((δ, δ 0 ), (, 0 )) | (δ, ) ∈ rI , (δ 0 , 0 ) ∈ rJ } for all r ∈ NR . A very helpful observation is that the classes of models of Horn (description) logics are closed under taking products [7]: given a Horn KB K and two interpretations I and J with I |= K and J |= K, it follows that I × J |= K. The next model transformation that we describe consists in picking one element and “copying” it (as well as all its atomic class memberships and relation to other elements) n times. Definition 4. Let n be a natural number, let I = (∆I , ·I ) be an interpretation and let δ ∈ ∆I . The n-fold duplication of δ in I creates an interpretation dupn (I, δ) = J with ∆J = ({0} × ∆I ) ∪ ({1 . . . n} × {δ}) as well as aJ = (0, aI ) for all a ∈ NI and for every predicate p of arity k holds ((n1 , δ1 ), . . . (nk , δk )) ∈ pJ if (δ1 , . . . , δk ) ∈ pI . Definition 5. We call a logic L non-counting, if modelhood is preserved under arbi- trary duplication of anonymous elements (i.e., elements δ ∈ ∆I with δ 6= aI for all a ∈ NI ). Note that FOL (without equality) is non-counting, and consequently all mainstream description logics without functionality and cardinality restrictions (that is, all DLs sub- sumed by SROI) are non-counting as well. Subsequent finding allows us to conclude NP-membership of satisfiability checking for a wide variety of (description) logics. Theorem 7. Let L be a non-counting Horn logic with bounded maximal predicate arity satisfying the polynomial nontrivial model property. Then fixed-domain satisfiability checking of L knowledge bases is in NP when using binary encoding. Proof. We describe a guess-and-check procedure. Let s be the prescribed domain cardi- nality and k = ||K|| be the size of the knowledge base. Let p be the polynomial as in the definition above. If s ≤ (p(k))2 , we guess and polytime-verify a model of size s (the guessed model takes polynomial space as L has bounded arity by assumption). Other- wise, we guess and polytime-verify a nontrivial model I of some cardinality s̃ ≤ p(k). It remains to show that the existence of I ensures the existence of a model J of cardinality s. Let I 0 = I × I. Obviously, I 0 has s̃2 ≤ (p(k))2 elements and is again a model (since L is a Horn logic by assumption). Also by construction, I 0 contains anonymous individuals (namely all elements of the form (δ, ) with δ 6= , existence guaranteed due to I being nontrivial). Let (δ, ) be one such anonymous individual. We obtain J by (s − s̃2 )-fold duplication of (δ, ). Since L is non-counting, J is a model of the knowledge base. t u Corollary 1. Fixed-domain satisfiability checking with binary encoding is in NP for the logics: bounded-arity Datalog, role-safety-acyclic (RSA) Horn-SHOI, EL++ with reflexivity and ranges, and all tractable profiles of OWL: OWL EL, OWL QL, and OWL RL. Table 1. Overview of fixed-domain standard reasoning complexities. Complexities marked with a star have been established in this paper for which pointers to the relevant theorems are given. s fixed Ref. unary Ref. binary Ref. finite ∗ DLmin NP [8] NP [8] NP Cor. 1 AC0 OWL QL NP [8] NP [8] NP ∗ Cor. 1 NL ∗ OWL RL NP [8] NP [8] NP Cor. 1 P ∗ ∗ ∗ EL terminologies NP Prop. 1 NP Prop. 1 NP Cor. 1 P OWL EL NP [8] NP [8] NP ∗ Cor. 1 P EL++ NP [8] NP [8] NP ∗ Cor. 1 P RSA Horn-SHOI NP [8] NP [8] NP ∗ Cor. 1 P ∗ ∗ ∗ ELI/ELF terminologies NP Prop. 1 NP Prop. 1 NE XP T IME Thm. 4, 5, 6 E XP T IME ∗ ALC NP [8] NP [8] NE XP T IME Thm. 4, 5 E XP T IME SHOIQ NP [8] NP [8] NE XP T IME ∗ Thm. 4, 5 NE XP T IME SROIQ NP [8] NP [8] NE XP T IME ∗ Thm. 4, 5 N2E XP T IME bounded-variable FOL(=) NP ∗ Thm. 3 NP ∗ Thm. 3 NE XP T IME ∗ Thm. 4, 5 undec. bounded-arity FOL(=) PS PACE ∗ Thm. 2 PS PACE ∗ Thm. 2 NE XP T IME ∗ Thm. 4, 5 undec. FOL (=) NE XP T IME Thm. 1, 4 NE XP T IME Thm. 1, 4 NE XP T IME ∗ Thm. 4, 5 ∗ ∗ undec. 6 Conclusion We investigated the complexities of standard reasoning under the fixed-domain seman- tics for first-order and a large range of description logics. We thereby specifically ac- count for the encoding of the imposed domain size, and distinguish between fixed, unary, and binary. Table 1 summarizes our findings. We obtain quite uniform results of NP-completeness on the full range of description logics for the case of a fixed or unary encoded domain size. Contrariwise, in case of a binary encoding, little expressiv- ity is needed to have standard reasoning jump to NE XP T IME where it remains for all formalisms subsumed by full first-order logic. Thus, regarding fixed-domain standard reasoning (i.e. satisfiability and non-entailment), we were able to complete the com- plexity landscape, and leave non-standard reasoning tasks, such as query answering as future work. Moreover, we consider a more fine granular investigation regarding data complexity. Acknowledgements This work is supported by DFG in the Research Training Group QuantLA (GRK 1763). We thank Franz Baader for asking the right questions, and are grateful for the valuable feedback from the anonymous reviewers, which helped greatly to improve this work. References 1. Baader, F., Brandt, S., Lutz, C.: Pushing the EL Envelope. In: Kaelbling, L.P., Saffiotti, A. (eds.), Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI 2005), Edinburgh, Scotland, UK, July 30 - August 5, 2005. pp. 364–369. Professional Book Center (2005) 2. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.: The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, second edn. (2007) 3. Baader, F., Lutz, C., Brandt, S.: Pushing the EL Envelope Further. In: Clark, K., Patel- Schneider, P.F. (eds.) Proceedings of the Fourth OWLED Workshop on OWL: Experiences and Directions, Washington, DC, USA, 1-2 April 2008. CEUR Workshop Proceedings, vol. 496. CEUR-WS.org (2008) 4. Baader, F., Sattler, U.: Expressive Number Restrictions in Description Logics. Journal of Logic and Computation 9(3), 319–350 (1999) 5. Calvanese, D.: Finite Model Reasoning in Description Logics. In: Padgham, L., Franconi, E., Gehrke, M., McGuinness, D.L., Patel-Schneider, P.F. (eds.) Proceedings of the International Workshop on Description Logics (DL 1996). AAAI Technical Report, vol. WS-96-05, pp. 25–36. AAAI Press (1996) 6. Carral, D., Feier, C., Grau, B.C., Hitzler, P., Horrocks, I.: Pushing the boundaries of tractable ontology reasoning. In: Mika, P., Tudorache, T., Bernstein, A., Welty, C., Knoblock, C.A., Vrandecic, D., Groth, P.T., Noy, N.F., Janowicz, K., Goble, C.A. (eds.) Proceedings of the 13th International Semantic Web Conference (ISWC2014), Riva del Garda, Italy, October 19-23, 2014. Proceedings, Part II. Lecture Notes in Computer Science, vol. 8797, pp. 148– 163. Springer (2014) 7. Chang, C., Keisler, H.J.: Model Theory, Studies in Logic and the Foundations of Mathemat- ics, vol. 73. North Holland, 3rd edn. (1990) 8. Gaggl, S.A., Rudolph, S., Schweizer, L.: Fixed-Domain Reasoning for Description Logics. In: Kaminka, G.A., Fox, M., Bouquet, P., Hüllermeier, E., Dignum, V., Dignum, F., van Harmelen, F. (eds.) Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI 2016). Frontiers in Artificial Intelligence and Applications, vol. 285, pp. 819 – 827. IOS Press (September 2016) 9. Horrocks, I., Kutz, O., Sattler, U.: The Even More Irresistible SROIQ. In: Doherty, P., My- lopoulos, J., Welty, C.A. (eds.) Proceedings of the 10th International Conference on Princi- ples of Knowledge Representation and Reasoning (KR 2006). pp. 57–67. AAAI Press (2006) 10. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexities of Horn Description Logics. ACM Transactions on Computational Logic (TOCL) 14(1), 2:1–2:36 (2013) 11. Lutz, C., Sattler, U., Tendera, L.: The complexity of finite model reasoning in description logics. Information and Computation 199(1-2), 132–171 (May 2005) 12. Papadimitriou, C.H.: Computational complexity. Addison-Wesley (1994) 13. Rosati, R.: Finite Model Reasoning in DL-Lite. In: Bechhofer, S., Hauswirth, M., Hoffmann, J., Koubarakis, M. (eds.) Proceedings of the 5th European Semantic Web Conference (ESWC 2008). LNCS, vol. 5021, p. 215. Springer (2008) 14. Rudolph, S.: Foundations of Description Logics. In: Polleres, A., d’Amato, C., Arenas, M., Handschuh, S., Kroner, P., Ossowski, S., Patel-Schneider, P.F. (eds.) Reasoning Web. 7th In- ternational Summer School 2011, Tutorial Lectures. LNCS, vol. 6848, pp. 76–136. Springer (2011) 15. Rudolph, S.: Undecidability Results for Database-Inspired Reasoning Problems in Very Ex- pressive Description Logics. In: Baral, C., Delgrande, J.P., Wolter, F. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Con- ference, KR 2016, Cape Town, South Africa, April 25-29, 2016. pp. 247–257. AAAI Press (2016) 16. Savitch, W.J.: Relationships Between Nondeterministic and Deterministic Tape Complexi- ties. Journal of Computer and System Sciences 4(2), 177–192 (Apr 1970) 17. Stockmeyer, L.J.: The Complexity of Decision Problems in Automata Theory and Logic. Ph.D. thesis, Massachusetts Institute of Technology (1974) 18. Tobies, S.: The Complexity of Reasoning with Cardinality Restrictions and Nominals in Expressive Description Logics. Journal of Artificial Intelligence Research (JAIR) 12, 199– 217 (2000)