=Paper=
{{Paper
|id=Vol-1265/paper9
|storemode=property
|title=All But Not Nothing: Left-Hand Side Universals for Tractable OWL Profiles
|pdfUrl=https://ceur-ws.org/Vol-1265/owled2014_submission_13.pdf
|volume=Vol-1265
|dblpUrl=https://dblp.org/rec/conf/owled/CarralKRH14
}}
==All But Not Nothing: Left-Hand Side Universals for Tractable OWL Profiles==
https://ceur-ws.org/Vol-1265/owled2014_submission_13.pdf
All But Not Nothing: Left-Hand Side Universals
for Tractable OWL Profiles
David Carral1 , Adila Krisnadhi1,2 , Sebastian Rudolph3 , and Pascal Hitzler1
1
Wright State University, Dayton, OH, U.S.A.
2
Universitas Indonesia, Depok, Indonesia
3
Technische Universität Dresden, Germany
Abstract. We show that occurrences of the universal quantifier in the
left-hand side of general concept inclusions can be rewritten into EL++
axioms under certain circumstances. I.e., this intuitive modeling feature
is available for OWL EL while retaining tractability. Furthermore, this
rewriting makes it possible to reason over corresponding extensions of
EL++ and Horn-SROIQ using standard reasoners.
1 Introduction
“All OWLED 2004 paper were written by George Lucas.”
The sentence just given is vacuously true since the OWLED conference series
was established in 2005, i.e., the statement is about the empty set: There are no
OWLED 2004 papers, hence all of them (namely, none) were written by George
Lucas.
Vacuously true statements arise from the formal semantics under which the
universal quantifier is interpreted in first-order predicate logic (and, more gener-
ally, in most of mathematics and computer science). This formal semantics gives
rise to a neat mathematical theory (e.g., the universal quantifier is then just
the dual of the existential quantifier), but at the same time this reading of the
universal quantifier remains rather unintuitive and also an educational obstacle
in the teaching of logic-based methods. In the Semantic Web realm, this was e.g.
prominently pointed out in [13], but examples of course abound.
Natural language use often does not intend vacuous truth. If John says “all
my children are adopted,” then we assume that he does in fact have children,
all of which are adopted. If we later found out that he never had any children,
then we may assess that he was lying earlier, rather than understand that his
statement was vacuously true.
More formally speaking, and in terms of description logic modeling, our in-
tuitive understanding would be that John belongs to the class
(∀hasChild.AdoptedPerson) u (∃hasChild.AdoptedPerson),
rather than simply ∀hasChild.AdoptedPerson which would seem more similar to
the natural language sentence on the syntax level. For lack of a better word, we
call such an occurrence of a universal a witnessed universal.
The observations just given are of course not at all new. And in fact, from
a formal logical perspective the observations do not even appear to be very
interesting at first sight: A witnessed universal simply seems to be syntactic
sugar because it can be expressed using a conjunction of a universal and an
existential.
However, it turns out that the discussion becomes much more interesting
in the context of logics – in this case description logics of course – where the
use of universal quantifiers is restricted in some way, i.e., for Horn Description
Logics and for some of the tractable OWL Profiles. Indeed, a version of witnessed
universal was investigated in [11],1 where it was shown that adding left-hand side
witnessed universals to Horn-SROIQ does not increase the data complexity.
The result was shown by a rather involved argument using a modification of the
SROIQ tableau algorithm.
However, we noticed that it is not necessary to modify the underlying rea-
soning algorithm, but that instead a simple knowledge base transformation can
be applied with which reasoning can be reduced to the case of knowledge bases
without universals. As a result, it is possible to add left-hand side witnessed
universals to OWL EL while retaining tractability. While we will later provide
a formal definition and correctness proof for the transformation, let us already
give an example which explains the rewriting. We want to model the statement
that a Pizza all of which toppings are vegetarian, is in fact a vegetarian Pizza.
Note, though, that the axiom ∀hasTopping.VegTopping v VegPizza does not suf-
ficiently capture the intended meaning, since a Pizza without any toppings (i.e.,
dough only) does hardly qualify as a Pizza in most people’s minds. An adequate
axiomatization thus seems to be
Pizza u (∀hasTopping.VegTopping) u (∃hasTopping.VegTopping) v VegPizza (1)
where the left-hand side does not suffer from the just mentioned vacuous truth
issue.
The rewriting which we introduce in this paper now rewrites this axiom into
the three axioms
Pizza u ∃hasTopping.VegTopping v ∃RPizza
∃hasTopping .>
RPizza
∃hasTopping v hasTopping
∃RPizza
∃hasTopping .VegTopping v VegPizza
where RPizza
∃hasTopping is a fresh role name. These axioms are expressible in ELH.
So in this paper, we report on this transformation, its correctness, and some
of its consequences. The plan of the paper is as follows. We first introduce some
formal preliminaries in Section 2. Then, in Section 3, we show our transformation
and prove it correct. We then make a proposal for an OWL/RDF and functional
style syntax for witnessed universals in Section 4, before we conclude in Section 5.
1
The conference presentation given for this paper was actually what made us start
thinking about the topic.
2 Preliminaries
In the following paragraphs we formally introduce the syntax, terminology and
semantics of the description logics EL++ and Horn-SROIQ as required for the
paper. We assume a certain familiarity with the topic and refer the reader to
the literature [1,3] if further background is required. To improve the readability
of the paper and the clarity of our formal arguments we make use of succinct
normal forms to describe the syntax of the aforementioned description logics.
This is without loss of generality: polynomial algorithms to normalize EL++
and Horn-SROIQ ontologies can be found in [7,8].
A DL signature is a tuple hNC , NR , NI i where NC , NR and NI are finite (but
large enough) disjoint sets of concept names, role names and individuals such
that {⊥, >} ⊆ NC . For the rest of this paper we assume that a signature Σ has
been fixed and so omit further references to it.
Let NR ∪ {R− | R ∈ NR } be the set of roles. Roles that are not elements of
NR are called inverse roles. A concept expression is a conjunction C1 u . . . u Cn
such that all C(i) are of the form ∃R.A, ∃R.Self, ran(R), ∀R.A, ≤ 1 R.A, A or
{a} where A ∈ NC , R ∈ NR and a ∈ NI . Concept expressions of the form {a}
are called nominals.
We define a function Inv that maps every role to its inverse counterpart, as
follows. (
R− , if R ∈ NR
Inv(R) =
S, R = S−
2.1 Syntax
A DL axiom is an expression as depicted in Figure 1. Given a set O of DL
axioms, we define the following notions.
– Let vO be the minimal relation over roles such that R vO S if R v S or
Inv(R) v Inv(S) are in O.
– Let v∗O be the reflexive transitive closure of vO .
– Let ≺O be the relation over roles such that R ≺O S and Inv(R) ≺O S if and
only if
• R 6= S,
• R 6= Inv(S), and
• R v S, R ◦ V v S or V ◦ R v S are in O.
– Let ≺∗O be the transitive closure of ≺O .
A role R is simple with respect to O if there is no axiom of the form T ◦ V v
S ∈ O for every role S such that S v∗O R or S v∗O Inv(R).
The DL EL++ . An EL++ axiom is an expression as depicted in the first four
columns of Figure 1. An EL++ ontology O is a set of EL++ axioms that satisfies
the following conditions.
A1 u . . . u An v B ∃R.A v B A v ∃S.B RvS R v S−
A1 u ∃R.A2 u ∀R.A3 v B ∃R.Self v B A v ∃S.Self R◦V vS A v ≤ 1 S.B
ran(R) v B {a} v B A v {b}
Fig. 1. DL Axioms. Where A(i) , B ∈ NC , R, S, V ∈ NR and a, b ∈ NI .
1. If ∃R.Self v B ∈ O, then R is simple.
2. If {R ◦ V v S, ran(S 0 ) v B} ⊆ O and S v∗O S 0 then ran(V ) v B ∈ O.
For a more comprehensive explanation of these restrictions, necessary to preserve
tractability of reasoning algorithms, see [2].
The DL Horn-SROIQ. A Horn-SROIQ axiom is an expression as depicted
Figure 1. A Horn-SROIQ ontology O is a set of Horn-SROIQ axioms that
satisfies the following conditions:
1. If ∃R.Self v B or A v ≤ 1 R.B are in O, then R is simple.
2. The relation ≺∗O is irreflexive.
Condition (2) is commonly referred as role regularity. For a more comprehensive
explanation of these restrictions, necessary to preserve decidability of reasoning
algorithms, see [5].
Note the we allow for axioms of the form A1 u ∃R.A2 u ∀R.A3 v B in our
definition of EL++ and Horn-SROIQ. These axioms are not usually considered
part of the definition of these languages [2,8], and they cannot be normalized
away using previous standard techniques.
2.2 Semantics
The semantics of an ontology is given through the definition of an interpretation
I = (∆I , ·I ) where ∆I is a set and ·I is a function that maps each individual in
the ontology to an element of ∆I , each concept name to a subset of ∆I and each
role name to a binary relation over ∆I . Interpretations are extended to concept
expressions as shown in the upper part of Figure 2. We say that an axiom α
is entailed by an interpretation I, written as I |= α, if the conditions defined
in the lower part of Figure 2 hold. An interpretation I satisfies an ontology O,
written as I |= O, if I |= α for every α ∈ O. If this is the case, we say that I is
a model of O. An ontology O entails an axiom α, written as O |= α, if I |= α
for every model I of O.
3 Witnessed Left-Hand Side Universals
We first define our new transformation that rewrites axioms of the form A1 u
∃R.A2 u ∀R.A3 v B into standard EL++ (and also Horn-SROIQ) axioms.
Constructor Syntax Semantics
Conjunction C1 u . . . u Cn C1I ∩ . . . ∩ CnI
Existential Restriction ∃R.A {x | ∃y : (x, y) ∈ RI , y ∈ DI }
Self Restriction ∃R.Self {x | (x, x) ∈ RI }
Range Restriction ran(R) {x | (y, x) ∈ RI }
Universal Restriction ∀R.A {x | ∀y : (x, y) ∈ RI , y ∈ DI }
At Most Restriction ≤ 1 R.A {x | ]{(x, y) ∈ RI | y ∈ AI } ≤ 1}
Nominal {a} {aI }
Top > ∆I
Bottom ⊥ ∅
Role Chain R◦V {(x, z) | (x, y) ∈ RI , (y, z) ∈ V I }
Inverse Role R {(x, y) | (y, x) ∈ Inv(R)I }
Axiom Syntax Semantics
Concept Inclusion CvD C I ⊆ DI
Role Inclusion RvS RI ⊆ S I
Role Chain Inclusion R◦V vS (R ◦ V )I ⊆ S I
Fig. 2. Semantics of DL Constructors and Axioms. Where x(i) , y, z ∈ ∆I , C(i) , D are
concept expressions, A ∈ NC , R(i) , S ∈ R, a, b ∈ NI and v ∈ NV
Definition 1. Let O be an EL++ or Horn-SROIQ ontology. Then O∀ is the
ontology that results from substituting every axiom α = A1 u ∃R.A2 u ∀R.A3 v
B ∈ O by axioms ∃R.A2 v Xα , A1 u Xα v Yα , Yα v ∃Zα .>, Zα v R and
∃Zα .A3 v B where Xα and Yα are fresh concepts and Zα is a fresh role.
We can verify that the transformation removes all universals while the output
stays within the base language.
Lemma 1. If O is an EL++ (respectively, Horn-SROIQ) ontology, then O∀ is
an EL++ (respectively, Horn-SROIQ) ontology without universal quantifiers.
Proof. It is straightforward to see that the axioms added by the transformation
are EL++ (respectively, Horn-SROIQ) axioms. Also, note that the newly added
axioms by the transformation do never violate any of the definining conditions
for language membership. In particular, not that a role R ∈ NR is simple with
respect to O∀ if and only if is simple with respect to O. Furthermore, note that
no axiom of the form R ◦ V v S, A v≤ 1R.B or ∃R.Self v B is added by the
transformation. t
u
Hence, after the transformation we can always make use of existing reason-
ing algorithms and tools for the appropriate description logic fragment. Also
note that the number of axioms added by the transformation is linear and thus
there are no implications for the complexity. Our central technical result is the
following.
Theorem 1. O and O∀ are equisatisfiable.
Proof. We first show how to construct a model J of O∀ given a model I of O.
Let ∆J = ∆I and ·J be as follows:
– For every a ∈ NI , aI = aJ .
– For every C ∈ NC , x ∈ C J if and only if x ∈ C I .
– For every R ∈ NR , (x, y) ∈ RJ if and only if (x, y) ∈ RI .
– For every α = A1 u ∃R.A2 u ∀R.A3 v B ∈ O and every x ∈ (∃R.A2 )I ,
x ∈ XαJ .
– For every α = A1 u ∃R.A2 u ∀R.A3 v B ∈ O and every x ∈ AI1 ∩ (∃R.A2 )I ,
x ∈ YαJ and
• if x ∈ (∀R.A3 )I then (x, y) ∈ ZαJ for some y such that (x, y) ∈ RI ,
• otherwise (x, y) ∈ ZαJ for some y such that (x, y) ∈ RI and y ∈ / AI3 .
Note that, given a model I, if some element x ∈ (AI1 ∩ (∃R.A2 )I ) \ (∀R.A3 )I
then there always exists some y ∈ ∆I such that (x, y) ∈ RI and y ∈ / AI3 .
We proceed to verify that J is indeed a model of O∀ . Note that, by definition,
J is identical to I when considering symbols that occur in O. Consequently, all
axioms that are in both O and O∀ are automatically entailed by J as they are
also entailed by model I. To verify that J is a model, we prove that all types of
axioms in O∀ which are not in O are indeed entailed by J . The different types
of axioms are as follows.
1. C1 u . . . u Cn v D ∈ O∀ \ O. Then C1 u . . . u Cn v D is of the form
A1 u Xα v Yα where α = A1 u ∃R.A2 u ∀R.A3 v B. Let x ∈ AJ J
1 ∩ Xα . Then
I I J
x ∈ A1 ∩ ∃R.A2 by the definition of J . Then x ∈ Yα also by the definition
of J .
2. V v S ∈ O∀ \O. Then V v S is of the form Zα v R where α = A1 u∃R.A2 u
∀R.A3 v B ∈ O. Let (x, y) ∈ ZαJ . Then (x, y) ∈ RJ by the definition of J .
3. ∃S.A v D ∈ O∀ \ O. Two cases arise:
– ∃S.A v D is of the form ∃R.A2 v Xα where α = A1 u ∃R.A2 u ∀R.A3 v
B ∈ O. Let (x, y) ∈ RJ and y ∈ AJ I
2 . Then x ∈ (∃R.A1 ) and x ∈ Xα
J
by the definition of J .
– ∃S.A v D is of the form ∃Zα .A3 v B where α = A1 u ∃R.A2 u ∀R.A3 v
B ∈ O. Let (x, y) ∈ ZαJ and y ∈ AJ 3 . Then, by the definition of J ,
x ∈ AI1 ∩ (∃R.A2 )I ∩ (∀S.A3 )I . Since I is a model and α ∈ O we have
that x ∈ B I . Consequently, x ∈ B J by the definition of J .
4. A v ∃R.B ∈ O∀ \ O. Then A v ∃R.B is of the form Yα v ∃Zα .>. Let
x ∈ YαJ . Then (x, y) ∈ Zα for some y by the definition of J .
We now show that every model J of O∀ is a model I of O. Not that for
every axiom α ∈ O that is not of the form A1 u ∃R.A2 u ∀R.A3 v B we have
that I |= α since α ∈ O∀ . Hence, it suffices to show that all axioms of the form
A1 u ∃R.A2 u ∀R.A3 v B are indeed entailed by I.
Let α = A1 u ∃R.A2 u ∀R.A3 v B ∈ O and x ∈ AI1 ∩ (∃R.A2 )I ∩ (∀R.A3 )I .
Then x ∈ AJ J J
1 ∩ (∃R.A2 ) ∩ (∀R.A3 ) . Note that {∃R.A2 v Xα , A1 u Xα v
Yα , Yα v ∃Zα .>, Zα v R, ∃Zα .A3 v B}. Since J is a model, we have that
x ∈ XαJ ∩ Yα and (x, y) ∈ ZαJ ∩ RJ for some y. Since x ∈ (∀R.A2 )J we have
that y ∈ AJ J I
2 . Thus, x ∈ B . Since I = J , x ∈ B and I |= ∃R.A1 u ∀R.A2 v B.
t
u
Note that solving other reasoning tasks for EL++ and Horn-SROIQ ontolo-
gies can be reduced to checking satisfiability. Therefore, our rewriting can also
be used to solve other tasks such as instance retrieval or classification.
4 OWL Syntax Extension
We propose an inclusion of the witnessed universal construct into OWL 2 through
several changes on the grammars of the different OWL 2 syntaxes. Before we
proceed, however, note that the transformation formulated in Section 3 was
defined for axioms with witnessed universal of the form A1 u ∃R.A2 u ∀R.A3 v
B where R, A1 , A2 , A3 and B are all atomic. This is nevertheless not a strict
limitation since arbitrary OWL 2 axioms in which such a witnessed universal
occurs within a subexpression and some of R, A1 , A2 , B are not atomic can still
be normalized so that witnessed universals only occur in axioms of the form
either A1 u ∃R.A2 u ∀R.A3 v B where R, A, A1 , A2 , A3 , B are all atomic. This
normalization is a simple variant of the standard structural transformation that
iteratively introduces definitions for non-atomic subexpressions in the original
axioms [6].
More importantly, this flexibility affords us to consider extending OWL 2
syntax with witnessed universals as a type of class expression, instead of having
to define a new type of OWL 2 axiom. The new syntactic element for witnessed
universal we shall present in this section is first and foremost just as a syntactic
shortcut for the corresponding OWL 2 class expression that uses conjunction, ex-
istential quantification, and universal quantification. Obviously, universal quan-
tification is not allowed in the tractable OWL 2 EL profile. With the result from
Section 3, we can now incorporate some form of universal quantification via the
new syntatic element, which we shall define in the rest of this section.
4.1 OWL 2 Functional-Style Syntax Modification
We start with the modification on the grammar of OWL 2 functional-style
syntax in Section 8.2 of [10]. Here, we introduce a new nonterminal symbol
ObjectSomeAllValuesFrom to represent a witnessed universal as a new type
of object property restrictions. Concretely, we first add the following production
rule to the grammar:
ObjectSomeAllValuesFrom := ’ObjectSomeAllValuesFrom’ ’(’
ObjectPropertyExpression ClassExpression ClassExpression’)’
We then add the nonterminal symbol ObjectSomeAllValuesFrom to the
ClassExpression production rule:
ClassExpression := Class | ObjectIntersectionOf | ObjectUnionOf |
ObjectComplementOf | ObjectOneOf | ObjectSomeValuesFrom |
ObjectAllValuesFrom | ObjectHasValue | ObjectHasSelf |
ObjectMinCardinality | ObjectMaxCardinality |
ObjectExactCardinality | DataSomeValuesFrom |
DataAllValuesFrom | DataHasValue | DataMinCardinality |
DataMaxCardinality | DataExactCardinality |
ObjectSomeAllValuesFrom
The ObjectSomeAllValuesFrom production rule above allows one to ex-
press an object property restriction ObjectSomeAllValuesFrom( OPE CE1 CE2 ),
which is a syntactic shortcut for the class expression
ObjectIntersectionOf( ObjectSomeValuesFrom( OPE CE1 )
ObjectAllValuesFrom( OPE CE2 ) ).
where both instances of the non-terminal OPE map to the same object property.
As an example, one can write axiom (1) from Section 1 using the OWL 2
functional-style syntax as follows:
SubClassOf(
ObjectIntersectionOf( a:Pizza
ObjectSomeAllValuesFrom( a:hasTopping a:VegTopping a:VegTopping ) )
a:VegPizza )
4.2 OWL 2 Manchester Syntax Modification
For the OWL 2 Manchester syntax [4], we only need to modify the production
rule for restriction into the rule below, using a new reserved word someall. As
in the functional-style syntax, the expression ( P someall C D ) is a syntactic
shortcut to the expression: ( P some C ) and ( P only D ).
restriction ::= objectPropertyExpression ’some’ primary
| objectPropertyExpression ’only’ primary
| objectPropertyExpression ’value’ individual
| objectPropertyExpression ’Self’
| objectPropertyExpression ’min’ nonNegativeInteger [ primary ]
| objectPropertyExpression ’max’ nonNegativeInteger [ primary ]
| objectPropertyExpression ’exactly’ nonNegativeInteger [ primary ]
| dataPropertyExpression ’some’ dataPrimary
| dataPropertyExpression ’only’ dataPrimary
| dataPropertyExpression ’value’ literal
| dataPropertyExpression ’min’ nonNegativeInteger [ dataPrimary ]
| dataPropertyExpression ’max’ nonNegativeInteger [ dataPrimary ]
| dataPropertyExpression ’exactly’ nonNegativeInteger [ dataPrimary ]
| objectPropertyExpression ’someall’ primary primary
Translation from Manchester syntax to functional-style syntax (and back)
is straightforward as in Section 4.2 and 4.3 of [4]. In particular, we add the
following row to the second table in Section 4.2 of the aforemetioned reference.
Nonterminal Form Transformation (T)
ObjectSomeAllValuesFrom(
objectPropertyExpression
restriction T(objectPropertyExpression)
someall primary primary
T(primary) T(primary))
4.3 Mapping to RDF Graphs in Turtle
We add the witnessed universal construct to the mappings from functional-style
syntax to RDF graphs in triple notation (Turtle), whose original document
is given in [12]. For brevity, we do not directly specify the OWL/XML and
RDF/XML serializations of witnessed universals, and simply assume that such
serializations are straightforward to obtain from the triple notation.
To add the witnessed universal construct to the mappings, we first add the
following row to the mapping from functional-style syntax to Turtle in Table 1
of [12].
Element E of the Structural Specifi- Main Node
Triples Generated in an Invocation T(E)
cation of T(E)
:x rdf:type owl:Restriction .
ObjectSomeAllValuesFrom( :x owl:onProperty T(OPE) .
:x
OPE CE1 CE2 ) :x owl:someAllValuesFrom
T(SEQ CE1 CE2 ) .
In the reverse mapping from Turtle to functional-style syntax, we add the
following row to Table 13 in [12].
If G contains this pattern... ...then CE( :x) is set to this class expression
:x rdf:type owl:Restriction .
:x owl:onProperty y . ObjectSomeAllValuesFrom( OPE(y) CE(z1 )
:x owl:someAllValuesFrom CE(z2 ) )
T(SEQ z1 z2 ) .
4.4 OWL 2 EL Syntax Modification
According to the formal grammar of OWL 2 EL (Section 2.2 in [9]), both of the
production rules for subClassExpression and superClassExpression pro-
duce the same set of class expression via the nonterminal ClassExpression.
The result in Section 3, however, implies that witnessed universal can only ap-
pear as a subclass expression in a class inclusion axiom in order to be included
to OWL 2 EL profile. This means that the production rules for subClassEx-
pression and superClassExpression need to produce different set of class
expressions, resulting in the following modified rules.
subClassExpression := Class | subObjectIntersectionOf | ObjectOneOf |
subObjectSomeValuesFrom | ObjectHasValue | ObjectHasSelf |
ObjectSomeAllValuesFrom | DataSomeValuesFrom | DataHasValue
subObjectIntersectionOf := ’ObjectIntersectionOf’ ’(’
subClassExpression subClassExpression { subClassExpression } ’)’
subObjectSomeValuesFrom := ’ObjectSomeValuesFrom’ ’(’
ObjectPropertyExpression subClassExpression ’)’
ObjectSomeAllValuesFrom := ’ObjectSomeAllValuesFrom’ ’(’
ObjectPropertyExpression subClassExpression subClassExpression ’)’
superClassExpression := Class | superObjectIntersectionOf | ObjectOneOf |
superObjectSomeValuesFrom | ObjectHasValue | ObjectHasSelf |
DataSomeValuesFrom | DataHasValue
superObjectIntersectionOf := ’ObjectIntersectionOf’ ’(’
superClassExpression superClassExpression { superClassExpression } ’)’
superObjectSomeValuesFrom := ’ObjectSomeValuesFrom’ ’(’
ObjectPropertyExpression superClassExpression ’)’
Notice that the difference between the production rules for subClassEx-
pression and superClassExpression only lies on the introduction of Object-
SomeAllValuesFrom. On the other hand, the production rules for Equiva-
lentClasses and DisjointClasses axioms need not be changed, i.e., they still
use the original production rule for ClassExpression.
5 Conclusions
While universal quantification is, in general, prohibited in EL++ and Horn-
SROIQ, we show that an intuitively rather appealing form of it, witnessed
universal quantification, can be added to both of these languages without jeop-
ardizing their pleasant computational properties. In particular, we show that
their left-hand side versions can be rewritten into the base languages.
We also provided a suggestion for an OWL syntax extension which could be
used as a basis for tool support for the new construct.
Acknowledgement This work was supported by the National Science Foun-
dation under award 1017225 “III: Small: TROn – Tractable Reasoning with
Ontologies” and the “La Caixa” foundation. Any opinions, findings, and conclu-
sions or recommendations expressed in this material are those of the author(s)
and do not necessarily reflect the views of the National Science Foundation.
References
1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.):
The Description Logic Handbook: Theory, Implementation, and Applications.
Cambridge University Press, second edn. (2007)
2. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proc. 19th Int.
Joint Conf. on Artificial Intelligence (IJCAI-05). pp. 364–369. Morgan-Kaufmann
Publishers, Edinburgh, UK (2005)
3. Hitzler, P., Krötzsch, M., Rudolph, S.: Foundations of Semantic Web Technologies.
Chapman & Hall/CRC (2009)
4. Horridge, M., Patel-Schneider, P. (eds.): OWL 2 Web Ontology Language Manch-
ester Syntax (Second Edition). W3C Working Group Note (11 December 2012),
available at http://www.w3.org/TR/owl2-manchester-syntax/
5. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Proc.
of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning
(KR 2006). pp. 57–67. AAAI Press (2006)
6. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: Brewka, G., Lang,
J. (eds.) Proc. 11th Int. Conf. on Principles of Knowledge Representation and
Reasoning (KR’08). pp. 274–284. AAAI Press (2008)
7. Krötzsch, M.: Efficient inferencing for OWL EL. In: Janhunen, T., Niemelä, I.
(eds.) Proc. 12th European Conf. on Logics in Artificial Intelligence (JELIA’10).
LNAI, vol. 6341, pp. 234–246. Springer (2010)
8. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexities of Horn description logics.
ACM Trans. Comp. Log. 14(1), 2:1–2:36 (2013)
9. Motik, B., Cuenca Grau, B., Horrocks, I., Wu, Z., Fokoue, A., Lutz, C. (eds.):
OWL 2 Web Ontology Language Profiles (Second Edition). W3C Recommendation
(27 October 2012), available at http://www.w3.org/TR/owl2-profiles/
10. Motik, B., Patel-Schneider, P., Parsia, B. (eds.): OWL 2 Web Ontology Lan-
guage Structural Specification and Functional-Style Syntax (Second Edition).
W3C Recommendation (11 December 2012), available at http://www.w3.org/TR/
owl2-syntax/
11. Nguyen, L.A., Nguyen, T.B.L., Szalas, A.: HornDL: An expressive Horn description
logic with PTime data complexity. In: Faber, W., Lembo, D. (eds.) Web Reasoning
and Rule Systems – 7th International Conference, RR 2013, Mannheim, Germany,
July 27-29, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7994, pp.
259–264. Springer (2013)
12. Patel-Schneider, P., Motik, B. (eds.): OWL 2 Web Ontology Language Mapping
to RDF Graphs (Second Edition). W3C Recommendation (11 December 2012),
available at http://www.w3.org/TR/owl2-mapping-to-rdf/
13. Rector, A.L., Drummond, N., Horridge, M., Rogers, J., Knublauch, H., Stevens,
R., Wang, H., Wroe, C.: OWL Pizzas: Practical experience of teaching OWL-
DL: Common errors & common patterns. In: Motta, E., Shadbolt, N., Stutt, A.,
Gibbins, N. (eds.) Engineering Knowledge in the Age of the Semantic Web, 14th
International Conference, EKAW 2004, Whittlebury Hall, UK, October 5-8, 2004,
Proceedings. Lecture Notes in Computer Science, vol. 3257, pp. 63–81. Springer
(2004)