We show that occurrences of the universal quanti er 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.
\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 quanti er is interpreted in rst-order predicate logic (and, more generally, in most of mathematics and computer science). This formal semantics gives rise to a neat mathematical theory (e.g., the universal quanti er is then just the dual of the existential quanti er), but at the same time this reading of the universal quanti er 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 intuitive understanding would be that John belongs to the class rather than simply 8hasChild: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 rst 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 quanti ers is restricted in some way, i.e., for Horn Description Logics and for some of the tractable OWL Pro les. 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 modi cation of the SROIQ tableau algorithm.
However, we noticed that it is not necessary to modify the underlying reasoning 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 de nition 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 8hasTopping:VegTopping v VegPizza does not sufciently 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 (8hasTopping:VegTopping) u (9hasTopping:VegTopping) v VegPizza (1) where the left-hand side does not su er from the just mentioned vacuous truth issue.
The rewriting which we introduce in this paper now rewrites this axiom into the three axioms
R9PhizazsaTopping v hasTopping
where R9PhizazsaTopping is a fresh role name. These axioms are expressible in E LH.
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 rst 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.
In the following paragraphs we formally introduce the syntax, terminology and
semantics of the description logics E L++ and Horn-SROIQ as required for the
paper. We assume a certain familiarity with the topic and refer the reader to
the literature [
A DL signature is a tuple hNC; NR; NIi where NC, NR and NI are nite (but large enough) disjoint sets of concept names, role names and individuals such that f?; >g NC. For the rest of this paper we assume that a signature has been xed and so omit further references to it.
Let NR [ fR j R 2 NRg 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 9R:A, 9R:Self, ran(R), 8R:A, 1 R:A, A or fag where A 2 NC, R 2 NR and a 2 NI. Concept expressions of the form fag are called nominals.
We de ne a function Inv that maps every role to its inverse counterpart, as follows.
Inv(R) = (R ; if R 2 NR
S; R = S 2.1
A DL axiom is an expression as depicted in Figure 1. Given a set O of DL axioms, we de ne 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 vO be the re exive 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 S 2 O for every role S such that S vO R or S vO Inv(R).
V v The DL EL++. An E L++ axiom is an expression as depicted in the rst four columns of Figure 1. An E L++ ontology O is a set of E L++ axioms that satis es the following conditions.
A1 u : : : u An v B A1 u 9R:A2 u 8R:A3 v B ran(R) v B
9R:A v B 9R:Self v B fag v B
A v 9S:B A v 9S:Self A v fbg
R
R v S
V v S
1. If 9R:Self v B 2 O, then R is simple.
2. If fR V v S; ran(S0) v Bg O and S vO S0 then ran(V ) v B 2 O.
For a more comprehensive explanation of these restrictions, necessary to preserve
tractability of reasoning algorithms, see [
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 satis es the following conditions: 1. If 9R:Self v B or A v 1 R:B are in O, then R is simple. 2. The relation is irre exive.
O
Condition (2) is commonly referred as role regularity. For a more comprehensive
explanation of these restrictions, necessary to preserve decidability of reasoning
algorithms, see [
Note the we allow for axioms of the form A1 u 9R:A2 u 8R:A3 v B in our
de nition of E L++ and Horn-SROIQ. These axioms are not usually considered
part of the de nition of these languages [
The semantics of an ontology is given through the de nition 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 j= , if the conditions de ned in the lower part of Figure 2 hold. An interpretation I satis es an ontology O, written as I j= O, if I j= for every 2 O. If this is the case, we say that I is a model of O. An ontology O entails an axiom , written as O j= , if I j= for every model I of O. 3
We rst de ne our new transformation that rewrites axioms of the form A1 u 9R:A2 u 8R:A3 v B into standard E L++ (and also Horn-SROIQ) axioms.
Constructor Syntax Conjunction C1 u : : : u Cn Existential Restriction 9R:A Self Restriction 9R:Self Range Restriction ran(R) Universal Restriction 8R:A At Most Restriction 1 R:A Nominal fag Top > Bottom ? Role Chain R V Inverse Role R Axiom Concept Inclusion Role Inclusion Role Chain Inclusion
Syntax C v D R v S R V v S
Semantics C1I \ : : : \ CnI fx j 9y : (x; y) 2 RI ; y 2 DI g fx j (x; x) 2 RI g fx j (y; x) 2 RI g fx j 8y : (x; y) 2 RI ; y 2 DI g fx j ]f(x; y) 2 RI j y 2 AI g faI g
I ; f(x; z) j (x; y) 2 RI ; (y; z) 2 V I g f(x; y) j (y; x) 2 Inv(R)I g De nition 1. Let O be an E L++ or Horn-SROIQ ontology. Then O8 is the ontology that results from substituting every axiom = A1 u 9R:A2 u 8R:A3 v B 2 O by axioms 9R:A2 v X , A1 u X v Y , Y v 9Z :>, Z v R and 9Z :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 E L++ (respectively, Horn-SROIQ) ontology, then O8 is an E L++ (respectively, Horn-SROIQ) ontology without universal quanti ers. Proof. It is straightforward to see that the axioms added by the transformation are E L++ (respectively, Horn-SROIQ) axioms. Also, note that the newly added axioms by the transformation do never violate any of the de nining conditions for language membership. In particular, not that a role R 2 NR is simple with respect to O8 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 9R:Self v B is added by the transformation. tu
Hence, after the transformation we can always make use of existing reasoning 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 O8 are equisatis able.
Proof. We rst show how to construct a model J of O8 given a model I of O. Let J = I and J be as follows: { For every a 2 NI, aI = aJ . { For every C 2 NC, x 2 CJ if and only if x 2 CI . { For every R 2 NR, (x; y) 2 RJ if and only if (x; y) 2 RI . { For every = A1 u 9R:A2 u 8R:A3 v B 2 O and every x 2 (9R:A2)I , x 2 XJ . { For every = A1 u 9R:A2 u 8R:A3 v B 2 O and every x 2 A1I \ (9R:A2)I , x 2 Y J and if x 2 (8R:A3)I then (x; y) 2 ZJ for some y such that (x; y) 2 RI , otherwise (x; y) 2 ZJ for some y such that (x; y) 2 RI and y 2= A3I . Note that, given a model I, if some element x 2 (A1I \ (9R:A2)I ) n (8R:A3)I then there always exists some y 2 I such that (x; y) 2 RI and y 2= A3I .
We proceed to verify that J is indeed a model of O8. Note that, by de nition, J is identical to I when considering symbols that occur in O. Consequently, all axioms that are in both O and O8 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 O8 which are not in O are indeed entailed by J . The di erent types of axioms are as follows. 1. C1 u : : : u Cn v D 2 O8 n O. Then C1 u : : : u Cn v D is of the form A1 u X v Y where = A1 u 9R:A2 u 8R:A3 v B. Let x 2 A1J \ XJ . Then x 2 A1I \ 9R:A2I by the de nition of J . Then x 2 Y J also by the de nition of J . 2. V v S 2 O8 nO. Then V v S is of the form Z v R where = A1 u9R:A2 u 8R:A3 v B 2 O. Let (x; y) 2 ZJ . Then (x; y) 2 RJ by the de nition of J . 3. 9S:A v D 2 O8 n O. Two cases arise: { 9S:A v D is of the form 9R:A2 v X where = A1 u 9R:A2 u 8R:A3 v B 2 O. Let (x; y) 2 RJ and y 2 A2J . Then x 2 (9R:A1)I and x 2 XJ by the de nition of J . { 9S:A v D is of the form 9Z :A3 v B where = A1 u 9R:A2 u 8R:A3 v B 2 O. Let (x; y) 2 ZJ and y 2 A3J . Then, by the de nition of J , x 2 A1I \ (9R:A2)I \ (8S:A3)I . Since I is a model and 2 O we have that x 2 BI . Consequently, x 2 BJ by the de nition of J . 4. A v 9R:B 2 O8 n O. Then A v 9R:B is of the form Y v 9Z :>. Let x 2 Y J . Then (x; y) 2 Z for some y by the de nition of J .
We now show that every model J of O8 is a model I of O. Not that for every axiom 2 O that is not of the form A1 u 9R:A2 u 8R:A3 v B we have that I j= since 2 O8. Hence, it su ces to show that all axioms of the form A1 u 9R:A2 u 8R:A3 v B are indeed entailed by I.
Let = A1 u 9R:A2 u 8R:A3 v B 2 O and x 2 A1I \ (9R:A2)I \ (8R:A3)I . Then x 2 A1J \ (9R:A2)J \ (8R:A3)J . Note that f9R:A2 v X ; A1 u X v Y ; Y v 9Z :>; Z v R; 9Z :A3 v Bg. Since J is a model, we have that
Note that solving other reasoning tasks for E L++ and Horn-SROIQ ontologies can be reduced to checking satis ability. Therefore, our rewriting can also be used to solve other tasks such as instance retrieval or classi cation. 4
We propose an inclusion of the witnessed universal construct into OWL 2 through
several changes on the grammars of the di erent OWL 2 syntaxes. Before we
proceed, however, note that the transformation formulated in Section 3 was
de ned for axioms with witnessed universal of the form A1 u 9R:A2 u 8R: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 9R:A2 u 8R: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 de nitions for non-atomic subexpressions in the original
axioms [
More importantly, this exibility a ords us to consider extending OWL 2 syntax with witnessed universals as a type of class expression, instead of having to de ne a new type of OWL 2 axiom. The new syntactic element for witnessed universal we shall present in this section is rst and foremost just as a syntactic shortcut for the corresponding OWL 2 class expression that uses conjunction, existential quanti cation, and universal quanti cation. Obviously, universal quanti cation is not allowed in the tractable OWL 2 EL pro le. With the result from Section 3, we can now incorporate some form of universal quanti cation via the new syntatic element, which we shall de ne in the rest of this section. 4.1
We start with the modi cation on the grammar of OWL 2 functional-style
syntax in Section 8.2 of [
ObjectPropertyExpression ClassExpression ClassExpression')' We then add the nonterminal symbol ObjectSomeAllValuesFrom to the
ClassExpression := Class j ObjectIntersectionOf j ObjectUnionOf j ObjectComplementOf j ObjectOneOf j ObjectSomeValuesFrom j ObjectAllValuesFrom j ObjectHasValue j ObjectHasSelf j ObjectMinCardinality j ObjectMaxCardinality j ObjectExactCardinality j DataSomeValuesFrom j DataAllValuesFrom j DataHasValue j DataMinCardinality j DataMaxCardinality j DataExactCardinality j
ObjectSomeAllValuesFrom
The ObjectSomeAllValuesFrom production rule above allows one to express 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 a:VegPizza )
ObjectSomeAllValuesFrom( a:hasTopping a:VegTopping a:VegTopping ) ) 4.2
For the OWL 2 Manchester syntax [
restriction ::= objectPropertyExpression 'some' primary j objectPropertyExpression 'only' primary j objectPropertyExpression 'value' individual j objectPropertyExpression 'Self' j objectPropertyExpression 'min' nonNegativeInteger [ primary ] j objectPropertyExpression 'max' nonNegativeInteger [ primary ] j objectPropertyExpression 'exactly' nonNegativeInteger [ primary ] j dataPropertyExpression 'some' dataPrimary j dataPropertyExpression 'only' dataPrimary j dataPropertyExpression 'value' literal j dataPropertyExpression 'min' nonNegativeInteger [ dataPrimary ] j dataPropertyExpression 'max' nonNegativeInteger [ dataPrimary ] j dataPropertyExpression 'exactly' nonNegativeInteger [ dataPrimary ] j 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 [
Nonterminal
Form restriction objectPropertyExpression someall primary primary
Transformation (T) ObjectSomeAllValuesFrom( T(objectPropertyExpression) T(primary) T(primary)) 4.3
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 rst add the following row to the mapping from functional-style syntax to Turtle in Table 1 of [12].
Element E of the Structural Speci - Triples Generated in an Invocation T(E) cation Main Node of T(E) ObjectSomeAllValuesFrom( OPE CE1 CE2 ) :x rdf:type owl:Restriction . :x owl:onProperty T(OPE) . :x owl:someAllValuesFrom T(SEQ CE1 CE2) .
:x
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... :x rdf:type owl:Restriction . :x owl:onProperty y . :x owl:someAllValuesFrom T(SEQ z1 z2) .
...then CE( :x) is set to this class expression ObjectSomeAllValuesFrom( OPE(y) CE(z1)
CE(z2) )
According to the formal grammar of OWL 2 EL (Section 2.2 in [
subClassExpression subClassExpression f subClassExpression g ')' subObjectSomeValuesFrom := 'ObjectSomeValuesFrom' '('
ObjectPropertyExpression subClassExpression ')' ObjectSomeAllValuesFrom := 'ObjectSomeAllValuesFrom' '('
ObjectPropertyExpression subClassExpression subClassExpression ')' superClassExpression := Class j superObjectIntersectionOf j ObjectOneOf j superObjectSomeValuesFrom j ObjectHasValue j ObjectHasSelf j DataSomeValuesFrom j DataHasValue superObjectIntersectionOf := 'ObjectIntersectionOf' '('
superClassExpression superClassExpression f superClassExpression g ')' superObjectSomeValuesFrom := 'ObjectSomeValuesFrom' '('
ObjectPropertyExpression superClassExpression ')'
Notice that the di erence between the production rules for subClassExpression and superClassExpression only lies on the introduction of ObjectSomeAllValuesFrom. On the other hand, the production rules for EquivalentClasses and DisjointClasses axioms need not be changed, i.e., they still use the original production rule for ClassExpression.
While universal quanti cation is, in general, prohibited in E L++ and HornSROIQ, we show that an intuitively rather appealing form of it, witnessed universal quanti cation, can be added to both of these languages without jeopardizing 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 Foundation under award 1017225 \III: Small: TROn { Tractable Reasoning with Ontologies" and the \La Caixa" foundation. Any opinions, ndings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily re ect the views of the National Science Foundation. 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 OWLDL: 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)