=Paper=
{{Paper
|id=Vol-1879/paper28
|storemode=property
|title=Not Too Big, Not Too Small... Complexities of Fixed-Domain Reasoning in First-Order and Description Logics
|pdfUrl=https://ceur-ws.org/Vol-1879/paper28.pdf
|volume=Vol-1879
|authors=Sebastian Rudolph,Lukas Schweizer
|dblpUrl=https://dblp.org/rec/conf/dlog/RudolphS17
}}
==Not Too Big, Not Too Small... Complexities of Fixed-Domain Reasoning in First-Order and Description Logics==
https://ceur-ws.org/Vol-1879/paper28.pdf
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)