It was mentioned on multiple occasions that datatype expressions are a necessary component of any production quality knowledge base and will surely play a major role in the upcoming Semantic Web. This paper briefly summarizes the work on improving the support for tractable reasoning with datatype expressions in ELK - a highly efficient reasoner. Tests have shown an exceptional speed of ontology classification of great size which opens up new perspectives for applying ontologies with datatype expressions in practice.
Background
In Description Logics, datatypes (also called concrete domains) can be used to define new concepts by referring to particular values, such as strings or integers. For example the following axioms from computer hardware ontology provide definitions for the notions of dual-, quad-, and many-core processors:
In mentioned example, , refers to the domain of natural numbers and the relation is used to constrain possible values to those larger than 1. Restriction , uses the relation to constrain the value to element 2, and similarly for , .
Any ontology reasoner, with a support of datatype expressions, as presented above, should be able to derive new axioms such as:
In order to ensure that reasoning remains polynomial, logic allows only for datatype restrictions that cannot implicitly express concept disjunction, which is a well-known cause of intractability. Consider, for example, the axioms: ∃. , ∃. , ≡ ⊓ ∃. ≡ ⊓ ∃. ≡ ⊓ ∃.
⊑ ⊑ It could be seen, that these axioms imply the disjunction:
⊑ ⊔
To prevent such situations, the EL Profile of OWL 2, which is based on , admits only equality in datatype restrictions. Unfortunately, it would be almost impossible to adequately model knowledge about real world domains using ontologies with such severe limitations on allowed datatype expressions.
It was recently demonstrated by D. Magka, Y. Kazakov and I. Horrocks [
But more work still needs to be done. Namely, a large amount of ontologies relies on other common datatypes, such as date/time, strings, binary data, URIs, etc: ∃. , .
Thus, a goal was set to use the approach, presented in [
Recent studies [
Newly developed reasoning procedures were implemented and tested in ELK – a
state of the art tractable reasoner [
Technical approach
According to Web Ontology Language specification, OWL 2 EL profile provides for 19 various datatypes, most of which are defined in XML Schema Definition Language (XSD) specification. Figure 1 provides a summary of all datatypes, allowed by the OWL 2 EL profile and displays their inheritance and a set of allowed facet restrictions.
It is worth mentioning, that OWL 2 EL profile does not allow the following datatypes: xsd:double, xsd:float, xsd:nonPositiveInteger, xsd:positiveInteger, xsd:negativeInteger, xsd:long, xsd:int, xsd:short, xsd:byte, xsd:unsignedLong, xsd:unsignedInt, xsd:unsignedShort, xsd:unsignedByte, xsd:language and xsd:boolean. The set of supported datatypes has been designed such that the intersection of the value spaces of any set of these datatypes is either empty or infinite, which is necessary to obtain the desired computational properties.
In order to support reasoning with abovementioned allowed datatypes, a set of new inference rules was implemented for the ELK reasoner:
C ⊑ ∃R. r
C ⊑ D ∃R. r ⊑ D ∈ , r
⊆ r C ⊑ ∃R. r ∈ , r
∅
C ⊑ where is an ontology, C and D are the concepts, R is a datatype property and ∃R. r denotes an existential datatype expression created with constraining facets. Symbols + and ̶ indicate that an expression is occurring right or left of ⊑ respectively.
With r ⊆ r we represent a fact that a value space constrained by the datatype restriction r is a subset of a value space constrained by the r datatype restriction, or in other words r includes r . With r ∅ we represent an empty value space produced by the datatype restriction r .
In the proposed implementation, all datatype expressions are parsed with respect to their lexical form and then transformed to internal representation that reflects the nature of their respective value space. All possible value spaces, created by the datatype restrictions, could be conventionally divided into 3 categories: • Values: binary value, date/time value, literal value and numeric value. • Intervals: numeric interval, date/time interval and length restriction • Other: empty value space, entire value space and pattern
During the computation of all conclusions under the inference rules, for each encountered ∃R. r expression a search is conducted for all ∃R. r expressions in the ontology where r ⊆ r . To increase the efficiency of reasoning, a special datatype index is used to optimize the search for all such ∃R. r expressions.
Table 1 summarizes all possible r ⊆ r scenarios where represents r datatype restriction, and represents r datatype restriction.
My means of B ⊆ A expression we state that the datatype of a restriction is equal to or inherited from the datatype of a restriction , for example xsd: integer ⊆ owl: real. Expression A and A denote a minimum and maximum value implied by the restriction , while B denotes a length of a corresponding value. Finally, by B → ∉ ∅ expression we represent a fact that literal value matches a corresponding pattern restriction . 3
Evaluation
The evaluation of proposed modifications was conducted using a large OWL 2 EL
ontology that was generated by the Grid-DL Semantic Grid information service [
Two test ontologies were considered. The full ontology consisted of 1,087,124 axioms, 65 classes, 33 object properties, 109 datatype properties and 131,637 individual assertions. Truncated version of the ontology connsisted of only 230,670 axioms and 36,191 individual assertions.
Three classes were added to act as a “query” to the knowledge base: UK_Site ≡ Site and hasLocation some
(Location and hasName some string[pattern ".*, UK"]) Idle_CE ≡ ComputingElement and hasState some (CEState and hasRunningJobs value 0 and hasWaitingJobs value 0 and hasFreeJobSlots some integer[>0]) and hasState some (CEState and hasStatus value Production) x64_Cluster ≡ SubCluster and (describedBy some (hasPlatformType value "x86_64"^^string) and (describedBy some (hasRAMSize some integer[>= 4096, <= 8192]))) ⊆ ⊆
A A B B A A
A A ⊆ ⊆
B
A ng ir - ⊆ - - - -
A ⊆
A A A
B B A A
A eum tren - ⊆ - - - - N I
B
B a P irc la v n th tio
c eL tse
R e l a In D c ir e N l a e L V e tea aV D
. re pS
. y p t S
V V
A 2 1 x i r t a m m o i t p u s b u s s n o i t c i r t s e r e p y t a t a e l b a T D В . 2
A e lu - ⊆ - - m a u V
B
A B A
B
A B
B A A
B B A A A A
- - w e i v A . А ) n . s n o i s s e r p x e r a l u g e r s a d e e r a s n o i t c i r t s e r l l o i t c i r t s e r ( n o i s s e r p x e r a l u g e r y f .e its p sa ty ll a i t a w d c )В i if n o i c e t sp i c r t t s s e o r m ( , n n o o is m se m r o p c x
e o t r t a s l a u
g c e e r ra fo s r n eb it
o m ta
e u r n p r e a t n n o i s y
r a e p v m a n b .
s o l u r e a r e ll o i b r d e t i l h id t s n o r c o e lf e 0 r
0 a y : t i l a u q a i E L
s 4 l 1 a r
e ± te re ir
e m t a o a u c th q g
y n if
r a u e
D V 3 4 r u e l - ⊆ - t i a -
⊆ ⊆ A
A
A B
B
B B im e A T lu - ⊆
A B B - - ⊆ - n
A ry e
A ian lau - ⊆ A B - - - B V
A B B
B ⊆
B B -
A in leu - ⊆ - - - - t E a pm leu - ⊆ - - - - E a
B A
B ty pS re S p e i p ray leu e Em laV u t n lu E a
V B in a
e a ti V ta
D e c im e la e ir e T lu r u e lu e la
m a V L V u V
N e l m a i v T r
e te t
Truncated ontology classification time, ms 7366 5598 165419 timeout
Full ontology classification time, ms 54912 12567 out of mem timeout
Unfortunately, HermiT reasoner could not classify the ontology within a 1 hour timeout constraint and Pellet ran out of memory while processing the full ontology. Evidently, ELK greatly outperformed abovementioned reasoners due to its efficient reasoning procedures.
The profiling analysis showed that it is possible to considerably speed up the reasoning procedures by using only one type of literals in the ontology, for example xsd:string. If such requirements are met, simplified literal handling algorithm could yield a considerable performance boost.
Currently the work is focused on designing and implementing an ontology analysis tool that would be capable of detecting unsafe datatype expressions in the processed ontology. It would ensure that ontology being reasoned upon does not contain conflicting datatype expressions that might cause incomplete results. In case if implicit disjunction is detected, a warning would be issued to the user, informing him about the source of the problem.
The source code of modified version of ELK with the support of tractable datatype reasoning can be found in elk-parent-datatypes branch in the official ELK repository: https://code.google.com/p/elk-reasoner. 4 5 Simplified literal reasoning algorithm