Bound Your Models!
How to Make OWL an ASP Modeling Language

arXiv:1511.00924v1 [] 3 Nov 2015

Sarah Alice Gaggl, Sebastian Rudolph, Lukas Schweizer
Technische Universität Dresden

Abstract. To exploit the Web Ontology Language OWL as an answer
set programming (ASP) language, we introduce the notion of bounded
model semantics, as an intuitive and computationally advantageous alternative to its classical semantics. We show that a translation into ASP
allows for solving a wide range of bounded-model reasoning tasks, including satisfiability and axiom entailment but also novel ones such as model
extraction and enumeration. Ultimately, our work facilitates harnessing
advanced semantic web modeling environments for the logic programming community through an “off-label use” of OWL.

Keywords: Answer Set Programming, Bounded-Model Semantics, Semantic
Web

1

Introduction

Answer set programming (ASP) is a powerful declarative language for knowledge
representation and reasoning [4]. In ASP the knowledge is encoded in a set of
logical rules and interpreted under the stable model semantics [8,9]. Recent developements led to powerful systems e.g. dlv [17], and gringo/clasp [6], to name
some of them, which are capable to solve a large variety of problems [7]. In particular, ASP has shown to be well suited for big combinatorial search problems,
as the dedicated solvers are specially designed to enumerate all solutions [2].
However, it has often been noted that, while being a powerful and versatile
formalism, popularity and widespread adoption of logic programming in general
and answer set programming in particular is hindered by the non-availability of
user-friendly and scalable editing environments.
On the other side, formalisms coming with a more elaborate modeling tool
support – most notably the Web Ontology Language OWL [31] – are often preferred, even if the application scenario actually is of a constraint-satisfaction type
which does not go well with OWL’s standard semantics allowing for models of
arbitrary size. Ontology editors like Protégé [16] provide user-friendly interfaces
and combined with the natural language alike Manchester syntax [12] possesses
perspicuous access to a presumably complex and involved formalism.
We propose bounded model reasoning as an intuitive and simple approach to
overcome this situation. Thereby, we endow OWL with a non-standard modeltheoretic semantics and modifying the modelhood condition by restricting the

domain to a finite set of bounded size, induced by the named individuals occurring in the given OWL ontology. We note that this additional condition can
be axiomatized in the latest version of OWL. While reasoning in OWL under
the classical semantics is N2ExpTime-complete [15], we show that reasoning
under the bounded model semantics is merely NP-complete. Still, employing the
axiomatization, existing OWL reasoners struggle on bounded model reasoning,
due to the heavy combinatorics involved.
Therefore, we propose a different approach and definine a translation of
SROIQ knowledge bases (the logical counterparts to OWL ontologies) into
answer set programs [4], such that the set of bounded models coincides with the
set of answer sets of the obtained program, allowing us to use existing answer
set solvers (see [2] for an overview) for bounded model reasoning. Next to the
inferencing tasks typically used in semantic web technologies, this approach also
allows for solving other, non-standard reasoning problems like model enumeration.
The benefits are manifolded, whereas in this work we particularly emphasize
OWL as modeling language for typical constraint-satisfaction-type problems.
The translation based approach can be seen as higher-level layer on top of the
ASP language. Although we focus on the description logic SROIQ and its native
DL syntax, other syntax specifications like the OWL 2 Manchester Syntax [12]
very well strive towards user-friendliness by means of natural language features.
We have implemented the proposed approach, for which first preliminary
evaluations on typical constraint-satisfaction-type problems not only demonstrate feasibility, but also suggest significant improvement compared to the axiomatized approach using highly optimized OWL reasoners.
The article is organized as follows. In Section 2 we introduce the necessary
background on description logics and ASP. Then, in Section 3 we define the
bounded model semantics and analyze their complexity. The particular encoding
of a SROIQ knowledge base into ASP is given in Section 4. A preliminary
evaluation of the implemented system is summarized in Section 5. Finally, we
conclude in Section 6 and discuss possible future directions.

2

Preliminaries

In this section we provide the necessary background of description logics and
answer set programming.
2.1

Description Logics

OWL 2 DL, the version of the Web Ontology Language we focus on, is defined
based on description logics (DLs, [3,25]). We briefly recap the description logic
SROIQ (for details see [13]). Let NI , NC , and NR be finite, disjoint sets called
individual names, concept names and role names respectively. These atomic entities can be used to form complex ones as displayed in Table 1. A SROIQ
knowledge base is a tuple (A, T , R) where A is a SROIQ ABox, T is a SROIQ
34

Table 1. Syntax and semantics of role and concept constructors in SROIQ, where
a1 , . . . an denote individual names, s a role name, r a role expression and C and D
concept expressions.
Name
Syntax
inverse role
s−
universal role
u
top
⊤
bottom
⊥
negation
¬C
conjunction
C ⊓D
disjunction
C ⊔D
nominals
{a1 , . . . , an }
univ. restriction ∀r.C
exist. restriction ∃r.C
Self concept
∃r.Self
qualified number 6n r.C
restriction
>n r.C

Semantics
{(x, y) ∈ ∆I × ∆I | (y, x) ∈ sI }
∆I × ∆I
∆I
∅
∆I \ C I
C I ∩ DI
C I ∪ DI
{aI1 , . . . , aIn }
{x | ∀y.(x, y) ∈ r I → y ∈ C I }
{x | ∃y.(x, y) ∈ r I ∧ y ∈ C I }
{x | (x, x) ∈ r I }
{x | #{y ∈ C I | (x, y) ∈ r I } ≤ n}
{x | #{y ∈ C I | (x, y) ∈ r I } ≥ n}

Table 2. Syntax and semantics of SROIQ axioms.
Axiom α
r1 ◦ · · · ◦ rn ⊑ r
Dis(s, r)
C⊑D
C(a)
r(a, b)
.
a=b
.
a 6= b

I |= α, if
r1I ◦ · · · ◦ rnI ⊆ r I
sI ∩ r I = ∅
C I ⊆ DI
aI ∈ C I
(aI , bI ) ∈ r I
a I = bI
aI 6= bI

RBox R
TBox T
ABox A

TBox and R is a SROIQ RBox. Table 2 presents the respective axiom types
available in the three parts, and we will refer to each TBox axiom as general concept inclusion (GCI). The original definition of SROIQ contained more RBox
axioms (expressing transitivity, (a)symmetry, (ir)reflexivity of roles), but these
can be shown to be syntactic sugar. Moreover, the definition of SROIQ contains so-called global restrictions which prevents certain axioms from occurring
together. These complicated restrictions, while crucial for the decidability of classical reasoning in SROIQ are not necessary for the bounded-model reasoning
considered here, hence we omit them for the sake of brevity.
The semantics of SROIQ is defined via interpretations I = (∆I , ·I ) composed of a non-empty set ∆I called the domain of I and a function ·I mapping
individual names to elements of ∆I , concept names to subsets of ∆I and role
names to subsets of ∆I × ∆I . This mapping is extended to complex role and
concept expressions (cf. Table 1) and finally used to define satisfaction of axioms
(see Table 2). We say that I satisfies a knowledge base K = (A, T , R) (or I is
a model of K, written: I |= K) if it satisfies all axioms of A, T , and R. We say
35

that a knowledge base K entails an axiom α (written K |= α) if all models of K
are models of α.
2.2

Answer-Set Programming

We give a brief overview of the syntax and semantics of disjunctive logic programs under the answer-sets semantics [9]. We fix a countable set U of (domain)
elements, also called constants; and suppose a total order < over the domain
elements. An atom is an expression p(t1 , . . . , tn ), where p is a predicate of arity n ≥ 0 and each ti is either a variable or an element from U. An atom is
ground if it is free of variables. BU denotes the set of all ground atoms over U.
A (disjunctive) rule ρ is of the form
a1 ∨ · · · ∨ an ← b1 , . . . , bk , not bk+1 , . . . , not bm ,
with n ≥ 0, m ≥ k ≥ 0, n + m > 0, where a1 , . . . , an , b1 , . . . , bm are atoms, or a
count expression of the form #count{l : l1 , . . . , li } ⊲⊳ u, where l is an atom and
lj = pj or lj = not pj , for pj an atom, 1 ≤ j ≤ i, u a non-negative integer, and
⊲⊳ ∈ {≤, <, =, >, ≥}. Moreover, “not ” denotes default negation. The head of ρ is
the set H(ρ) = {a1 , . . . , an } and the body of ρ is B(ρ) = {b1 , . . . , bk , not bk+1 , . . . ,
not bm }. Furthermore, B + (ρ) = {b1 , . . . , bk } and B − (ρ) = {bk+1 , . . . , bm }. A rule
ρ is normal if n ≤ 1 and a constraint if n = 0. A rule ρ is safe if each variable
in ρ occurs in B + (r). A rule ρ is ground if no variable occurs in ρ. A fact is a
ground rule with empty body and no disjunction. An (input) database is a set of
facts. A program is a finite set of rules. For a program Π and an input database
D, we often write Π(D) instead of D ∪ Π. If each rule in a program is normal
(resp. ground), we call the program normal (resp. ground).
For any program Π, let UΠ be the set of all constants appearing in Π. Gr (Π)
is the set of rules ρσ obtained by applying, to each rule ρ ∈ Π, all possible
substitutions σ from the variables in ρ to elements of UΠ . For count-expressions,
{l : l1 , . . . , ln } denotes the set of all ground instantiations of l, governed through
{l1 , . . . , ln }. An interpretation I ⊆ BU satisfies a ground rule ρ iff H(ρ) ∩ I 6= ∅
whenever B + (ρ) ⊆ I, B − (ρ) ∩ I = ∅, and for each contained count-expression,
N ⊲⊳ u holds, where N is the cardinality of the set of ground instantiations of
l, N = |{l | l1 , . . . , ln }|, for ⊲⊳ ∈ {≤, <, =, >, ≥} and u a non-negative integer.
I satisfies a ground program Π, if each ρ ∈ Π is satisfied by I. A non-ground
rule ρ (resp., a program Π) is satisfied by an interpretation I iff I satisfies all
groundings of ρ (resp., Gr (Π)). I ⊆ BU is an answer set of Π iff it is a subsetminimal set satisfying the Gelfond-Lifschitz reduct Π I = {H(ρ) ← B + (ρ) |
I ∩ B − (ρ) = ∅, ρ ∈ Gr (Π)}. For a program Π, we denote the set of its answer
sets by AS(Π).

3

Bounded Models

When reasoning in description logics, models can be of arbitrary cardinality.
In many applications, however, the domain of interest is known to be finite. In
36

fact, restricting DL reasoning to models of finite domain size (called finite model
reasoning, a natural assumption in database theory), has become the focus of
intense studies lately [18,5,24].
As opposed to assuming the domain to be merely finite (but of arbitrary,
unknown size), we consider the case where the domain has an a priori known
cardinality, more precisely, when the domain coincides with the set of named
individuals mentioned in the knowledge base. We refer to such models as bounded
models and argue that in many applications this modification of the standard
DL semantics represents a more intuitive definition of what is considered and
expected as model of some knowledge base.1
Definition 1 (Bounded-Model Semantics). Let K be a SROIQ knowledge
base. An interpretation I = (∆I , ·I ) is said to be individual-bounded w.r.t. K,
if all of the following holds:
1. ∆I = {a | a ∈ NI (K)},
2. for each individual a ∈ NI (K), aI = a.
Accordingly, we call an interpretation I (individual-)bounded model of K, if I
is an individual-bounded interpretation w.r.t. K and I |= K holds. A knowledge
base K is called bounded-model-satisfiable if it has a bounded model. We say K
bounded-model-entails an axiom α (written K |=bm α) if every bounded model
of K is also a model of α.
Note that, under the bounded-model semantics, there is a one-to-one correspondence between (bounded) interpretations and sets of ground facts, if one assumes
the set of domain elements fixed and known. That is, for every bounded-model
interpretation I = (∆I , ·I ), we find exactly one Abox AI with atomic concept
assertions and role assertions defined by AI := {r(a, b) | (a, b) ∈ rI } ∪ {A(a) |
a ∈ AI } and likewise, every such Abox A gives rise to a corresponding interpretation I A . This allows us to use ABoxes as representations of models.
We briefly demonstrate the effects of bounded model semantics as opposed
to finite model semantics (with entailment |=fin ) and the classical semantics. Let
K = (A, T , R) with A = {A(a), A(b), s(a, b)}, T = {⊤ ⊑ ∃r.B, ⊤ ⊑ 61 r− .⊤},
and R = {Dis(s, r)}. First we note that K has a bounded (hence finite) model I
representable as AI = {A(a), A(b), B(a), B(b), s(a, b), r(a, a), r(b, b)}, thus K is
satisfiable under all three semantics. Then α = ⊤ ⊑ ∃r.∃r.B holds in all models
of K, therefore K |= α, K |=fin α, and K |=bm α. Opposed to this, β = ⊤ ⊑ B
merely holds in all finite models, whence K |=fin β and K |=bm β, but K 6|= β.
Finally, γ = ⊤ ⊑ ∃r.Self only holds in all bounded models, thus K |=bm γ, but
K 6|=fin γ and K 6|= γ.
1

In fact, when working with practicioners performing modeling tasks in OWL, we often found this to be their primary intuition, and OWL to be “abused” as a constraint
language for an underlying fixed domain.

37

3.1

Extraction & Enumeration of Bounded Models

When performing satisfiability checking in DLs (the primary reasoning task considered there), a model constructed by a reasoner merely serves as witness to
claim satisfiability, rather than an accessible artifact. However, as mentioned before, our approach aims at scenarios where a knowledge base is a formal problem
description for which each model represents one solution. Then, retrieval of one,
several, or all models is a natural task, as opposed to merely checking existence.
With model extraction we denote the task of materializing an identified model
in order to be able to work with it, i.e. to inspect it in full detail and reuse it in
downstream processes. The natural continuation of model extraction is to make
all models explicit, performing model enumeration. Conveniently, for both tasks
we can use the introduced model representation via ABoxes.
Most existing DL reasoning algorithms attempt to successively construct a
model representation of a given knowledge base. However, most of the existing
tableaux reasoners do not reveal the constructed model, besides the fact that in
the non-bounded case models might end up being infinite such that an explicit
representation is impossible. Regarding enumeration, we state that this task
is not supported – not even implicitly – by any state-of-the-art DL reasoner,
also due to the reason that in the non-bounded case, the number of models
is typically infinite and even uncountable. We want to stick to the notions of
model extraction and enumeration as their meaning should be quite intuitive.
Although, in the general first-order case the term model expansion is used, e.g. in
the work of Mitchell and Ternovska [19]. There, an initial (partial) interpretation
representing a problem instance is expanded to ultimately become a model for
the encoded problem.
3.2

Complexity of Bounded Model Reasoning

The combined complexity of reasoning in SROIQ over arbitrary interpretations
is known to be N2ExpTime-complete [15]. Still, it is considered to be usable
in practice since worst-case knowledge bases would be of very artificial nature.
Restricting to bounded models leads to a drastic drop in complexity.
Theorem 1. The combined complexity of checking bounded-model satisfiability
of SROIQ knowledge bases is NP-complete.
Proof. (Sketch) To show membership, we note that after guessing an interpretation I, (bounded) modelhood can be checked in polynomial time. For this we
let C contain all the concept expressions occurring in K (including subexpressions). Furthermore, let R contain all role expressions and role chains (including
subchains) occurring in K. Obviously, C and R are of polynomial size. Then,
in a bottom-up fashion, we can compute the extension C I of every element C
of C and the extension rI of every element r of R along the defined semantics.
Obviously, each such computation step requires only polynomial time. Finally,
based on the computed extensions, every axiom of K can be checked – again in
polynomial time.
38

To show hardness, we note that any 3SAT problem can be reduced to boundedmodel satisfiability asVfollows: Let L = {L1 , . . . , Ln } be a set of 3-clauses.
Then satisfiability of {ℓ1 ,ℓ2 ,ℓ3 }∈L (ℓ1 ∨ ℓ2 ∨ ℓ3 ) coincides with the boundedmodeldsatisfiability of the knowledge base containing the two axioms ⊤(a) and
⊤ ⊑ {ℓ1 ,ℓ2 ,ℓ3 }∈L (Cℓ1 ⊔ Cℓ2 ⊔ Cℓ3 ), where Cℓi = Ap if ℓi = p and Cℓi = ¬Ap if
ℓi = ¬p for any propositional symbol p.
Note that this finding contrasts with the observation that bounded-model
reasoning in first-order logic is PSpace-complete. We omit the full proof here,
just noting that membership and hardness can be easily shown based on the
fact that checking modelhood in FOL is known to be PSpace-complete [30]
and, for the membership part, keeping in mind that NPSpace=PSpace thanks
to Savitch’s Theorem [28]. This emphasizes the fact that, while the boundedmodel restriction turns reasoning in FOL decidable, restricting to SROIQ still
gives a further advantage in terms of complexity (assuming P 6= NP).
3.3

Axiomatization of Bounded Models inside SROIQ

When introducing a new semantics for some logic, it is worthwhile to ask if existing reasoners can be used. Indeed, it is easy to see that, assuming {a1 , . . . , an } =
NI (K), adding the SROIQ GCI ⊤ ⊑ {a1 , . . . , an } as well as the set of inequality axioms containing ai 6≈ aj with i < j to K will rule out exactly all the
non-bounded models of K. Denoting these additional axioms with BM, we then
find that K is bounded-model satisfiable iff K ∪ BM is satisfiable under the classical DL semantics and, likewise, K |=bm α iff K ∪ BM |= α for any axiom α.
Consequently, any off-the-shelf SROIQ reasoner can be used for bounded-model
reasoning, at least when it comes to the classical reasoning tasks.
However, the fact that the currently available DL reasoners are not optimized
towards reasoning with axioms of the prescribed type (featuring disjunctions
over potentially large sets of individuals) and that available reasoners do not
support model extraction and model enumeration led us to develop an alternative
computational approach based on ASP.

4

Encoding SROIQ Knowledge Bases into ASP

We propose an encoding of an arbitrary SROIQ knowledge base K, into an
answer set program Π(K), such that the set of answer sets AS(Π(K)), coincides
with the set of bounded models of the given knowledge base. This allows us
to use existing ASP machinery to perform both standard reasoning as well as
model extraction and model enumeration quite elegantly. Intuitively, the set of
all bounded models defines a search space, which can be traversed searching for
models, guided by appropriate constraints. We thus propose an ASP encoding
consisting of a generating part Πgen (K), defining all potential candidate interpretations, and a constraining part Πchk (K), ruling out interpretations violating
the knowledge base.
39

Table 3. Ω-Normalization of knowledge base axioms.
Ω(K) =

[

α∈R∪A

Ω(α) ∪

[

Ω(⊤ ⊑ nnf(¬C1 ⊔ C2 ))

C1 ⊑C2 ∈T

Ω(⊤ ⊑ C ⊔ C ′ ) = Ω(⊤ ⊑ C ⊔ αC ′ ) ∪

[

Ω(⊤ ⊑ ¬α
˙ C ′ ⊔ Ci )

1≤i≤n
′

for C ′ of the form C = C1 ⊓ · · · ⊓ Cn and n ≥ 2
Ω(⊤ ⊑ C ⊔ ∀r.D) = Ω(⊤ ⊑ C ⊔ ∀r.αD ) ∪ Ω(⊤ ⊑ ¬α
˙ D ⊔ D)
Ω(⊤ ⊑ C ⊔ ≥ n r.D) = Ω(⊤ ⊑ C ⊔ ≥ n r.αD ) ∪ Ω(⊤ ⊑ ¬α
˙ D ⊔ D)
Ω(⊤ ⊑ C ⊔ ≤ n r.D) = Ω(⊤ ⊑ C ⊔ ≤ n r.¬α
˙ ¬D
˙ ¬D
⊔ ¬D)
˙
˙ ) ∪ Ω(⊤ ⊑ ¬α
˙

⊥
if C = ∅,
Ω(⊤ ⊑ C ⊔ ¬{s}) =
Ω(C(s)) otherwise.
Ω(D(s)) = {αD (s)} ∪ Ω(⊤ ⊑ ¬α
˙ D ⊔ nnf(D))
Ω(r − (s, t)) = {r(t, s)}
Ω(r1 ◦ . . . ◦ rn ⊑ r) = {r1 ◦ r2 ⊑ r(r1◦r2 ) } ∪ Ω(r(r1◦r2 ) ◦ r3 ◦ . . . ◦ rn ⊑ r)
for any RIA with n > 2
Ω(β)
=
{β}
for
any
other
axiom
β

QC if pos(C) = true
αC =
, where QC is a fresh concept name unique for C
¬QC if pos(C) = false
pos(⊥) = false
pos(⊤) = false
pos(¬A) = false
pos(A) = true
pos(¬{s}) = false
pos({s}) = true
pos(¬∃r.Self ) = false
pos(∃r.Self ) = true
pos(C1 ) ∨ pos(C2 )
pos(C1 ⊓ C2 ) = pos(C1 ) ∨ pos(C2 ) pos(C1 ⊔ C2 ) = 
pos(¬C
˙ 1 ) if n = 0
pos(∀r.C1 ) = pos(C1 )
pos(≤ n r.C1 ) =
true
otherwise
pos(≥ n r.C1 ) = true
Note: A is an atomic concept, C(i) are arbitrary concept expressions, C is a possibly
empty disjunction of concept expressions, D is not a literal concept. The function ¬˙
is defined as ¬(¬A)
˙
= A and ¬(A)
˙
= ¬A for some atomic concept A.

Our translation into ASP requires a knowledge base in normal form which
can be obtained by an easy syntactic transformation.
DefinitionF2 (Normalized Form [22]). A GCI is normalized, if it is of the
n
form ⊤ ⊑ i=1 Ci , where Ci is of the form B, {a}, ∀r.B, ∃r.Self , ¬∃r.Self ,
≥ n r.B, or ≤ n r.B, for B a literal concept, r a role, and n a positive integer. A
TBox T is normalized, if each GCI in T is normalized. An ABox A is normalized
if each concept assertion in A contains only a literal concept, each role assertion
in A contains only an atomic role, and A contains at least one assertion. An
RBox R is normalized, if each role inclusion axiom is of the form r ⊑ r′ or
r1 ◦ r2 ⊑ r′ . A SROIQ knowledge base K = (A, T , R) is normalized if A, T ,
and R are normalized.
Given K = (A, T , R), the normalized form Ω(K) is obtained by applying a
transformation Ω, given in Table 3, which is mainly standard in DLs [22]. The
normalized knowledge base Ω(K) is a model-conservative extension of K, i.e.
every (bounded) model of Ω(K) is a (bounded) model of K and every (bounded)
model of K can be turned into a (bounded) model of Ω(K) by finding appropriate
40

interpretions for the concepts and roles introduced by Ω. Thereby it is straightforward to extract a model for K, given a model of Ω(K). In the remainder, we
will assume a knowledge base in normalized form, if not stated otherwise.

4.1

Candidate Generation

As shown, any potential bounded interpretation I B is induced by a set of individual assertions B, such that for each concept name A, role name r and individuals a, b occurring in K, either A(a) ∈ B, or ¬A(a) ∈ B and either r(a, b) ∈ B
or ¬r(a, b) ∈ B. This construction is straightforward to encode via subsequent
rules:
{A(X) :− not ¬A(X), ⊤(X) | A ∈ NC (K)} ∪

Πgen (K) :=

(1)

{¬A(X) :− not A(X), ⊤(X) | A ∈ NC (K)} ∪

(2)

{ar (r, X, Y ) :− not ¬ar (r, X, Y ), ⊤(X), ⊤(Y ) | r ∈ NR (K)} ∪

(3)

{¬ar (r, X, Y ) :− not ar (r, X, Y ), ⊤(X), ⊤(Y ) | r ∈ NR (K)} ∪

(4)

{⊤(a) | a ∈ NI (K)}.

(5)

Recall, that a rule is unsafe, if a variable that occurs in the head does not
occur in any positive body literal. The predicate ⊤(X) ensures safe rules, each
of the guessing rules (1–4) would otherwise be unsafe. This predicate represents
the ⊤-concept, to which the statement (5) asserts each individual present in
K. The function ar takes care of potential inverse roles (cf. Table 4). Whereas
“not ” denotes default negation, ¬ is without attached semantics and merely
used as syntactic counterpart to the DL vocabulary. We show now that Πgen (K)
computes BK , the set of all constructible B, and each B ∈ BK determines a
solution of Πgen (K).
Proposition 1 (BK = AS(Πgen (K))). Let K = (A, T , R) be a SROIQ knowledge base and Πgen (K) the logic program obtained by the translation given in
(1–5). Then, it holds that BK coincides with the set of all answer sets of Πgen (K).

4.2

Axiom Encoding

In the next step, we turn each axiom α ∈ R ∪ T into a constraint, ultimately
ruling out those candidate interpretations not satisfying α. Moreover, each individual assertion in the ABox A restricts the search space further, since for some
present fact A(a) any solution candidate containing ¬A(a) is eliminated. We will
successively introduce appropriate encodings for axioms of each knowledge base
component, altogether manifested in the program Πchk (K) and will finally show
that the program Π(K) = Πgen (K) ∪ Πchk (K) computes all bounded models of
K.
41

Encoding TBox Axioms Since T is normalized, each GCI is of certain form which
simplifies the encoding. We obtain Πchk (T ) as follows:
Πchk (T ) :=

n
G

{:− trans(C1 ), . . . , trans(Cn ) | for each ⊤ ⊑

Ci in T }

(6)

i=1

Each concept expression Ci is translated according to the function trans(Ci )
depicted in Table 4. Note, each Ci is only one of the ones given in Definition
2, the ones given in the first column; i.e. not complex, with the nice effect of
trans(Ci ) to be realized non-recursively.
Table 4. Translation of Concept Expressions.
C
trans (C)
A
not A(X)
¬A
A(X)
{a}
{not Oa (X)}, {Oa (a)}
∀r.A
{not A(YA ), ar (r, X, YA )}
∀r.¬A
{ar (r, X, YA ), A(YA )}
∃r.Self
not ar (r, X, X)
¬∃r.Self
ar (r, X, X)
≥ n r.A
#count {ar (r, X, YA ) : A(YA )} < n
≥ n r.¬A #count {ar (r, X, YA ) : not A(YA )} < n
≤ n r.A
#count {ar (r, X, YA ) : A(YA )} > n
≤ n r.¬A #count {ar (r, X, YA ) : not A(YA )} > n
Note: Oa is a new concept name
unique for a. And ar (r, X, Y ) is defined as follows:

r(X, Y ) if r is an atomic role
ar (r, X, Y ) :=
s(Y, X) if r is an inverse role and r = s−

Encoding RBox Axioms Role assertions and role inclusion axioms are also transformed into constraints, grouped in the program Πchk (R). According to their DL
semantics, this yields:
Πchk (R) := {:− ar (r, X, Y ), not ar (s, X, Y ) | r ⊑ s ∈ R} ∪
{:− ar (s, X, Y ), ar (r, X, Y ) | Dis(r, s) ∈ R} ∪

(7)
(8)

{:− ar (s1 , X, Y ), ar (s2 , Y, Z), not ar (r, X, Z) |s1 ◦ s2 ⊑ r ∈ R}.
(9)
Encoding ABox Axioms The ABox A itself represents an input database, which
we can directly use. However, it remains to check whether A does not contain
contradictory knowledge; i.e. propositional clashes of the form {A(a), ¬A(a)} ∈
A. Hence, the program Πchk (A) consists of A and one additional constraint for
each concept and role name ruling out inconsistent input ABoxes.
Πchk (A) := A ∪

(10)

{:− A(X), ¬A(X) | A ∈ NC (K)} ∪
{:− ar (r, X, Y ), ¬ar (r, X, Y ) | r ∈ NR (K)}.
42

(11)
(12)

Note that the presence of {A(a), ¬A(a)} ∈ A does not cause an unsatisfiable
program under the answer set semantics, since ¬ does not have any meaning
under the semantics; ¬A is treated as just another predicate name. Thus, the
imposed constraints simulate the known DL semantics.
Theorem 2. Let K = (A, T , R) be a normalized SROIQ knowledge base, and
Π(K) = Πgen (K) ∪ Πchk (K) be the program obtained by applying Rules (1–12).
Then, it holds:
AS(Π(K)) = {B | B ∈ BK and I B |= K}
With this theorem in place, we benefit from the translation in many aspects.
Most notably, in addition to the standard DL reasoning tasks, model extraction
and model enumeration can be carried out without additional efforts, since both
are natural tasks for answer set solvers.

5

Evaluation

We implemented our approach as an open-source tool, named Wolpertinger.2
The obtained logic programs can be evaluated with most modern ASP solvers.
However, the evaluation was conducted using Clingo [6] for grounding and solving, since it currently is the most prominent solver leading the latest competitions [2]. We present preliminary evaluation results based on simple ontologies,
encoding constraint-satisfaction-type combinatorial problems. Existing OWL ontologies typically used for benchmarking, e.g. SNOMED or GALEN [29,23], do
not fit our purpose, since they are modeled with the classical semantics in mind
and often have little or no ABox information.
Our tests provide runtimes of Wolpertinger and the popular HermiT reasoner [10]. Whereas a direct comparison would not be fair, the conducted tests
shall merely show the feasibility of our approach and the infeasibility of the axiomatization using standard DL reasoners. The evaluation itself is conducted on
a standard desktop machine.3
5.1

Unsatisfiability

We construct an unsatisfiable knowledge base Kn = (An , T n , ∅), with T n and An
as follows:
T n = {A1 ⊑ ∃r.A2 , . . . , An ⊑ ∃r.An+1 } ∪

(13)

{Ai ⊓ Aj ⊑ ⊥ | 1 ≤ i < j ≤ n + 1}
An = {A1 (a1 ), ⊤(a1 ), . . . , ⊤(an )}

(14)
(15)

Inspired by common pigeonhole-type problems, we have Kn enforce an r-chain
of length n + 1 without repeating elements, yet, given only n individuals such a
2
3

https://github.com/wolpertinger-reasoner
Unix operating system, 1.8 Ghz Intel Core i7 Processor, 4 GB memory. Both tools
are executed with standard Java-VM settings.

43

Table 5. Runtime comparison for detecting unsatisfiability of Kn .
# Nominals Concepts Wolpertinger HermiT #Backtrackings
1
5
6
< 0, 001 s
000, 148 s
260
2
6
7
< 0, 001 s
000, 436 s
1.630
3
7
8
000, 040 s
001, 050 s
11.742
4
8
9
000, 320 s
002, 292 s
95.900
5
9
10
004, 790 s
015, 301 s
876.808
6
10
11
054, 400 s
144, 024 s
8.877.690
7
11
12
085, 080 s
> 15 min
> 50 × 106

Table 6. Enumerating Sudoku Instances – Runtime Overview.
# Models Requested Time(Total) Time(Solving)
1
100
006, 014 s
000, 130 s
2
1.000
006, 372 s
000, 560 s
3
10.000
008, 558 s
002, 800 s
4
100.000
034, 096 s
027, 960 s
5
1.000.000
279, 059 s
273, 150 s

model cannot exist. Table 5 depicts the runtimes for detecting unsatisfiability of
Kn , for increasing n. The durations correspond to the pure solving time of Clingo
and pure reasoning time of HermiT, respectively, as both Wolpertinger and
HermiT have a comparable preprocessing. As the figures suggest, Kn is a potential
worst-case scenario, where both tools are doomed to test all combinations. On
this task, Wolpertinger constantly outperforms HermiT. For K11 , HermiT is
stopped after 15 minutes, whereas Wolpertinger detects unsatisfiability within
85 seconds.

5.2

Model Extraction and Model Enumeration

With Table 6, we next provide some figures for model extraction and partial
enumeration (retrieving a given number of bounded models). To this end, we
created a knowledge base modeling fully and correctly filled Sudokus, featuring
108 named individuals, 13 concept names and 1 role name. When invoking a
satisfiability test on this knowledge base using HermiT, no answer was given
within 15 minutes.
On average, Wolpertinger provides a solution for a given Sudoku instance
in around 6 seconds, of which more than 5 seconds are needed for grounding,
while the actual solving is done in less than 0.1 seconds. For model enumeration,
we used the knowledge base but removed information concerning pre-filled cells,
turning the task into generating new Sudoku instances. The size of the grounded
program is 13 MB, the grounding process taking around 6 seconds as reflected
in Table 6.
44

6

Conclusion

With this paper, we have established the starting point for further developments
on the theoretical and practical side, as well as we can identify benefits for
both, the description logic and logic programming community. For the latter,
our approach enables one to use OWL as ASP modeling language and therefore
make use of the available tool support. Although modeling features are limited,
we argue that quite large and involved problem scenarios can be modeled in OWL
ontologies. Clearly, evaluations of our system with respect to such ontologies
remain as imperative issue.
Complementarily, model extraction and enumeration supplement DL reasoning tasks for which our ASP translation represents not only a feasible approach,
but apparently also a use case of ASP in another research field. Moreover, the
framework may be extended to realize non-standard reasoning tasks useful for
debugging purposes such as axiom pinpointing, explanation, justification and
abduction, exploiting the innate capabilities of ASP to realize minimization as
well as model enumeration.
On a more practical level, the proposed translation can certainly be optimized
to exploit more built-in features of today’s ASP solvers. In terms of harnessing
the convenience of OWL modeling environments, we will implement an OWL
API reasoner interface for Wolpertinger, such that it can e.g., be seamlessly be
integrated with other OWL software, such as Protégé [16].
Regarding future theoretical DL investigations, in recent years, significant
extensions of the modeling and querying capabilities of DLs have been proposed
and partially implemented. A major such extension is considering the reasoning
task of answering queries, most prominently (unions of) conjunctive queries, positive queries, conjunctive 2-way regular path queries, and monadically defined
queries subsuming all of the former [27]. It is not overly difficult to show that
answering all these query types over SROIQ knowledge bases (and hence over
OWL ontologies) under the bounded model semantics is ΠP2 -complete, which
again contrasts with the much worse results (if any) for the unbounded case
[26,11]. Moreover, as all these query formalisms can be straightforwardly expressed in a rule-based way, an integration in our framework is immediate. In
the same way, rule-based extensions of OWL – monotonic [14,21] or nonmonotonic [20,1] – should be straightforward to accommodate, at the cost of the
combined complexity jumping to ExpTime or NExpTime.

Acknowledgements
We are grateful for all the valuable feedback from our colleagues and the anonymous workshop reviewers, which helped greatly to improve this work.
45

References
1. Alferes, J.J., Knorr, M., Swift, T.: Query-Driven Procedures for Hybrid MKNF
Knowledge Bases. ACM Transactions on Computational Logic 14(2), 16:1–16:43
(2013)
2. Alviano, M., Calimeri, F., Charwat, G., Dao-Tran, M., Dodaro, C., Ianni, G.,
Krennwallner, T., Kronegger, M., Oetsch, J., Pfandler, A., Pührer, J., Redl, C.,
Ricca, F., Schneider, P., Schwengerer, M., Spendier, L.K., Wallner, J.P., Xiao,
G.: The Fourth Answer Set Programming Competition: Preliminary Report. In:
Cabalar, P., Son, T.C. (eds.) Proc. of the 12th International Conference on Logic
Programming and Nonmonotonic Reasoning (LPNMR 2013). LNCS, vol. 8148, pp.
42–53. Springer (2013)
3. 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)
4. Brewka, G., Eiter, T., Truszczyński, M.: Answer set programming at a glance.
Commun. ACM 54(12), 92–103 (2011)
5. Calvanese, D.: Finite model reasoning in description logics. In: Proc. of the International Workshop on Description Logics (DL 1996). pp. 25–36 (1996)
6. Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Schneider,
M.: Potassco: The Potsdam Answer Set Solving Collection 24(2), 107–124 (2011)
7. Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning 6, 1–238
(2012)
8. Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In:
Kowalski, R.A., Bowen, K.A. (eds.) Proc. of the 5th International Conference and
Symposium on Logic Programming. pp. 1070–1080. MIT Press (1988)
9. Gelfond, M., Lifschitz, V.: Classical Negation in Logic Programs and Disjunctive
Databases. New Generation Comput. 9(3/4), 365–386 (1991)
10. Glimm, B., Horrocks, I., Motik, B., Stoilos, G., Wang, Z.: HermiT: an OWL 2
reasoner. Journal of Automated Reasoning 53(3), 245–269 (2014)
11. Glimm, B., Kazakov, Y., Lutz, C.: Status QIO: An Update. In: Rosati, R., Rudolph,
S., Zakharyaschev, M. (eds.) Proc. of the 24th International Workshop on Description Logics (DL 2011). CEUR Workshop Proceedings, vol. 745. CEUR-WS.org
(2011)
12. Horridge, M., Patel-Schneider, P.F.: OWL 2 Web Ontology Language Manchester
Syntax (2012)
13. Horrocks, I., Kutz, O., Sattler, U.: The Even More Irresistible SROIQ. In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) Proc. of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR 2006). pp.
57–67. AAAI Press (2006)
14. Horrocks, I., Patel-Schneider, P.F., Boley, H., Tabet, S., Grosof, B.N., Dean, M.:
SWRL: A Semantic Web Rule Language. W3C Member Submission (21 May 2004)
15. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: Brewka, G., Lang,
J. (eds.) Proc. of the 11th International Conference on Principles of Knowledge
Representation and Reasoning (KR 2008). pp. 274–284. AAAI Press (2008)
16. Knublauch, H., Musen, M.A., Rector, A.L.: Editing Description Logic Ontologies
with the Protégé OWL Plugin. In: Haarslev, V., Möller, R. (eds.) Proc. of the
International Workshop on Description Logics (DL 2004). CEUR Workshop Proceedings, vol. 104. CEUR-WS.org (2004)

46

17. Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The
DLV System for Knowledge Representation and Reasoning. ACM Trans. Comput.
Log. 7(3), 499–562 (2006)
18. 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)
19. Mitchell, D.G., Ternovska, E.: A framework for representing and solving NP search
problems. In: Proc. of AAAI. vol. 5, pp. 430–435 (2005)
20. Motik, B., Rosati, R.: Reconciling description logics and rules. Journal of the ACM
57(5) (2010)
21. Motik, B., Sattler, U., Studer, R.: Query Answering for OWL DL with Rules.
Journal of Web Semantics 3(1), 41–60 (2005)
22. Motik, B., Shearer, R., Horrocks, I.: Hypertableau Reasoning for Description Logics. Artificial Intelligence Research 36, 165–228 (2009)
23. Rector, A., Horrocks, I.: Experience building a large, re-usable medical ontology
using a description logic with transitivity and concept inclusions. In: Proc. of the
Workshop on Ontological Engineering (1997)
24. Rosati, R.: Finite Model Reasoning in DL-Lite. In: Bechhofer, S., Hauswirth, M.,
Hoffmann, J., Koubarakis, M. (eds.) Proc. of the 5th European Semantic Web Conference on The Semantic Web: Research and Applications (ESWC 2008). LNCS,
vol. 5021, p. 215. Springer (2008)
25. 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 International Summer School 2011, Tutorial Lectures. LNCS,
vol. 6848, pp. 76–136. Springer (2011)
26. Rudolph, S., Glimm, B.: Nominals, Inverses, Counting, and Conjunctive Queries
or: Why Infinity is your Friend! Journal of Artificial Intelligence Research 39, 429–
481 (2010)
27. Rudolph, S., Krötzsch, M.: Flag & Check: Data Access with Monadically Defined
Queries. In: Hull, R., Fan, W. (eds.) Proc. of the 32nd Symposium on Principles
of Database Systems (PODS’13). pp. 151–162. ACM (2013)
28. Savitch, W.J.: Relationships Between Nondeterministic and Deterministic Tape
Complexities. J. Comput. Syst. Sci. 4(2), 177–192 (Apr 1970)
29. Spackman, K.A., Campbell, K.E., Côté, R.A.: SNOMED RT: a reference terminology for health care. In: AMIA 1997, American Medical Informatics Association
Annual Symposium. AMIA (1997)
30. Stockmeyer, L.J.: The Complexity of Decision Problems in Automata Theory and
Logic. Ph.D. thesis, Massachusetts Institute of Technology (1974)
31. W3C OWL Working Group: OWL 2 Web Ontology Language: Document
Overview. W3C Recommendation, http://www.w3.org/TR/owl2-overview (2009)

47

A

Proofs

Proof of Theorem 2 By Proposition 1, Πgen (K) computes the set BK . It remains
to show, that Πchk (K) obeys the bounded model semantics, and consequently
excludes each B ∈ BK not inducing a bounded model I B .
AS(Π(K)) ⊆ {B | B ∈ BK and I B |= K} Let I ∈ AS(Π(K)) be an answer
set of Π(K). From Proposition 1, we know I ∈ BK . We show now that the
interpretation I I induced by I is a bounded model of K, and therefore I I |= α,
for each axiom α ∈ K. Then, let
α ∈ R: we distinguish role disjointness, and role inclusion axioms:
α ∈ Ra : Let α = Dis(r, s) ∈ Ra , then by definition of Πchk (R), there
is a ground constraint ρα = :− s(a, b), r(a, b) in Gr (Πchk (R)), for all
individuals a, b ∈ NI (K). Since I is an answer set, {s(a, b), r(a, b)} 6∈ I.
Consequently either (a, b) ∈ sI I , or (a, b) ∈ rI I , hence I I |= Dis(r, s).
α ∈ Rh : then let α be of the form s1 ◦ s2 ⊑ r, with s1 , s2 , r ∈ NR (K),
and ρα = :− s1 (a1 , a2 ), s2 (a2 , a3 ), not r(a1 , a3 ) be the ground constraint
in Gr (Πchk (R)). Since I is an answer set, we have that, if s1 (a1 , a2 ) and
s2 (a2 , a3 ) ∈ I implies r(a1 , a3 ) ∈ I. And consequently (a1 , a2 ) ∈ s1 I I ,
(a2 , a3 ) ∈ s2 I I and (a1 , a3 ) ∈ rI I , thus I I |= s1 ◦F
s2 ⊑ r.
n
α ∈ T : then α is normalized and of the form ⊤ ⊑ i=1 Ci . In Rule (6), α
is turned into a constraint ρα = :− trans(C1 ), . . . , trans(Cn ) in Πchk (T ).
Since I is an answer set, it does not violate any of the grounded instances
of ρα in Gr (Πchk (T )). Suppose now towards contradiction, I I induced by
I does not satisfy α, I I 6|= α. Then, I I 6|= Ci , for all 1 ≤ i ≤ n. However,
since I does not violate ρα , in each of the ground instantiations of ρα , there
is exists a trans(Ci ) which is not satisfied by I, 1 ≤ i ≤ n. Then, Ci is one
of the expressions given in Definition 2, and we distinguish:
Ci = A: then trans(Ci ) = not A(X), and A(a) ∈ I for any a ∈ NI (K).
Consequently a ∈ AI I 6= ∅, which contradicts the assumption I I 6|= Ci .
Ci = ¬A: then trans(Ci ) = A(X), and ¬A(a) ∈ I for any a ∈ NI (K).
Consequently a ∈ (¬A)I I 6= ∅, which contradicts the assumption I I 6|=
Ci .
Ci = {a}: then trans(Ci ) = {not Oa (X)} and Oa (a), thus necessarily
Oa (a) ∈ I. In order to not satisfy trans(Ci ), X = a. Consequently we
have a ∈ OaI I with Oa as nominal guard concept, and therefore {a}II =
{a}, which contradicts the assumption.
Ci = ∀r.A: then trans(Ci ) = {r(X, YA ), not A(Ya )}, and A(b) ∈ I whenever r(a, b) ∈ I. Consequently, (a, b) ∈ rI I implies b ∈ AI I , which contradicts the assumption I I 6|= Ci .
Ci = ≥ n r.A: then trans(Ci ) = #count{r(X, YA ) : A(YA )} < n, and
more or equal than n, say m, atoms r(a, b) ∈ I and A(b) ∈ I. Consequently we find also m pairs (a, b) ∈ rI I and b ∈ AI I , which contradicts
the assumption.
All remaining cases can be treated analogously.
48

α ∈ A: I satisfies Πchk (A), in particular A ⊆ I. Moreover, none of the
imposed constraints in Πchk (A) is violated, proving consistency of A, and
therefore {A(a), ¬A(a)} 6∈ I and {r(a, b), ¬r(a, b)} 6∈ I for all concept names
A ∈ NC (K), role names r ∈ NR (K) and individuals a, b ∈ NI (K).
AS(Π(K)) ⊇ {B | B ∈ BK and I B |= K} Let I B be a bounded model of K,
induced by some B ∈ BK . We show that B is an answer set of Π(K) = Πgen (K)∪
Πchk (K). From Proposition 1 we know, that B is an answer set of Πgen (K), thus
it remains to show that B satisfies Πchk (K) and therefore does not violate any
of the imposed constraints. Since I B |= α, for each α ∈ K, let
α ∈ R: we distinguish again role disjointness and role chain axioms.
α ∈ Ra : Let α = Dis(r, s) ∈ Ra and ρα = r(X, Y ), s(X, Y ), be the
constraint according to Rule (8). Since I B |= α, for all a, b ∈ NI (K) we
find, that {r(a, b), s(a, b)} 6∈ B, and consequently none of the grounded
instances of ρα is violated by B.
α ∈ Rh : then α is of the form s1 ◦ s2 ⊑ r, with s1 , s2 , r ∈ NR (K),
and ρα = :− s1 (X, Y1 ), s2 (Yn , Z), not r(X, Z) is the constraint according
to Rule (9). Since I B |= α, for all a1 , a2 , a3 ∈ NI (K) we have that if
s1 (a1 , a2 ) and sn (a2 , a3 ) ∈ B, then r(a1 , a3 ) ∈ B. Consequently, ρα is
not violated by B.
F
α ∈ T : then α is normalized and of the form ⊤ ⊑ ni=1 Ci , which is satisfied
by I B , iff CiI B 6= ∅ for some 1 ≤ i ≤ n. Let ρα = :− trans(C1 ), . . . , trans(Cn )
be the constraint obtained from α, applying Rule (6). We need to show that
B does not violate the constraint. Let Ci be the concept expression for which
CiI B 6= ∅ holds, 1 ≤ i ≤ n, and Ci is one of the expressions given in Definition
2, in particular we have:
Ci = A: then AI B = {a | A(a) ∈ B}. Consequently, for each of those
A(a) ∈ B, trans(A) = not A(X) is not satisfied.
Ci = ¬A: then ¬AI B = {a | ¬A(a) ∈ B}. Consequently, for each of those
¬A(a) ∈ B, trans(¬A) = A(X) is not satisfied.
Ci = ∃r.Self : then (∃r.Self )I I = {a | r(a, a) ∈ B}. Consequently,
trans(∃r.Self ) = not r(X, X) is not satisfied for those r(a, a) ∈ B.
Ci =≤ r n.A: then (≤ r n.A)I B = {a | #{r(a, b) and A(b) ∈ B} = m ≤
n}. Consequently, trans(≤ r n.A) = #count{r(X, YA ) : A(YA )} > n, is
not satisfied since there are m such r(a, b) ∈ B with A(b) ∈ B.
All remaining cases can be treated analogously.
α ∈ A: then α ∈ B, as well as α ∈ Πchk (A), since by definition A ∈ Πchk (A).
In general, since I B |= K, A is consistent and therefore {A(a), ¬A(a)} 6∈ B,
as well as {r(a, b), ¬r(a, b)} 6∈ B for all concept names A, role names r and
individuals a, b.


49

