EL

Overview

EL++ is a lightweight description logic that admits sound and complete reasoning in polytime. It is a syntactic fragment of OWL 1.1 DL. In particular, it shares the semantics of OWL 1.1 DL. The design goals behind EL++ were two-fold:

• capture the expressive power that is used by large-scale ontologies from practical applications
• have polytime reasoning problems, in particular classification and instance checking

EL++ indeed achieves both goals in a very natural way. A main characteristics of EL++ is to drop the (allValuesFrom) restriction, whereas (someValuesFrom) is retained. This is in contrast to fragments such as DL Lite [1], in which (someValuesFrom) is also dropped. However, it should be noted that EL++ does admit (objectPropertyRange), which can be seen as an important special case of (allValuesFrom).

Among the ontologies that fall within EL++ are the following:

• SNOMED CT, the Systematized Nomenclature of Medizine, Clinical Terms. SNOMED is a large-scale commercial ontology that underlies the standardized terminology of the health-care systems in the US, the UK, and a couple of other countries. It comprises about half a million classes. For more information, see [2] and [3].
• NCI. The Thesaurus of the National Cancer Institute. An ontology that formalizes terms related to cancer research. Like SNOMED, it is constantly updated and extended. Comprises about 50000 classes. For more info, see [4].
• The Gene Ontology formalizes terms relating to genes and gene products. Currently comprises some 25000 classes. For more info, see [5].

More than 95% of the axioms of the GALEN ontology [6] can also be expressed in EL++.

A polytime classification algorithm for EL++ ontologies has been implemented in the CEL reasoner [7], which is freely available. CEL is capable of classifying large-scale ontologies such as SNOMED in only a few minutes. Note that this refers to ontology classification, not querying of instance data. It is likely that, using database technology, querying instance data w.r.t. EL++ ontologies can be carried out even much more efficiently.

Our experience with CEL suggests that reasoning with polytime fragments of OWL DL is much more robust than reasoning in full OWL-DL in the following sense: whereas reasoners for full OWL DL can often also classify large-scale ontologies after having been optimized by their system designers for the specific ontology at hand, polytime reasoners can usually classify large scale ontologies formulated in their restrictive language out of the box, i.e., without specific tuning of the reasoner.

Other implementations of EL++ reasoning include the one by the Australian E-Health research center [8] and by Arity corporation [9], see also [10] for the latter.

There are a couple of different versions of EL++. As a fragment of OWL, there is a unique version of EL++ that comes up naturally. The proposal is to include only this one version of EL++ in the OWL standard. This version is described in the remainder of this document. All of the reasoning problems classification, subsumption, satisfiability, and instance checking are polytime.

Language Overview

EL++ provides the following main features:

• someValuesFrom restrictions,
• conjunction
• concept disjointness,
• hasValue restrictions
• oneOf enumerations involving a single element,
• complex inclusions between object properties (where complex refers to the fact that property chains may be used on the left-hand side),
• reflexive properties,
• transitive properties,
• domain and range restrictions on properties,
• a limited form of datatypes, and
• general concept inclusion axioms (GCIs).

The following features of OWL 1.1 are known to cause intractability, when added to EL++:

• allValuesFrom restrictions,
• cardinality restrictions,
• union (and also DisjointUnion),
• negation,
• inverse properties,
• symmetric properties,
• functional and inverse-functional properties, and
• oneOf enumerations involving multiple elements.

Definition in Terms of Functional Syntax

In what follows, a full specification of EL++ is provided.

Class Descriptions and Object Properties

Entities are defined just as in OWL 1.1. The definition of objectPropertyExpression simplifies to

since we do not admit InverseObjectProperty. Class descriptions are built according to the following grammar:

The classes owl:Thing and owl:Nothing are both admitted.

Missing w.r.t. OWL 1.1 DL: objectUnionOf, objectComplementOf, objectOneOf with multiple elements, objectAllValuesFrom, objectMaxCardinality, objectMinCardinality, objectExactCardinality

Axioms

Annotation is as in OWL 1.1, and is dropped from the grammars for readability.

Class Axioms

Missing w.r.t. OWL 1.1 DL: disjointUnion

Property Axioms

Missing w.r.t. OWL 1.1 DL: disjointObjectProperties, irreflexiveObjectProperty, inverseObjectProperties, functionalObjectProperty, symetricObjectProperty, asymetricObjectProperty.

It is likely that we can also allow irreflexiveObjectProperty and disjointObjectProperty (and maybe also asymetricObjectProperty), but details remain to be checked (if worthwhile).

Facts

Regarding facts, EL++ provides exactly the same facilities as OWL 1.1 DL. Again, annotations are as in OWL 1.1, but not listed in the grammar for simplicity.

Class Assertions

Property Assertions

Nonstructural Restrictions on Axioms

To obtain polytime reasoning problems, the axiom closure of an EL++ ontology must obey a certain nonstructural restriction, which is defined next. The reason for this restriction is a subtle interaction between role inclusions and range restrictions, which has to be controlled. Let us say that an EL++ ontology entails the axiom ObjectPropertyRange(PE1 CE) if its axiom closure contains axioms

• SubObjectPropertyOf(PE1 PE2),...,SubObjectPropertyOf(PEk-1 PEk)
• ObjectPropertyRange(PEk CE)

Then the restriction is as follows:

If

• the ontology contains SubObjectPropertyOf(SubObjectPropertyChain(PE1 ... PEn) PE) and
• the ontology entails ObjectPropertyRange(PE CE)

then the ontology entails ObjectPropertyRange(PEn CE).

Observe that the restriction is vacuously tree if the SubObjectPropertyOf is a role inclusion statement, i.e., if it does not contain SubObjectPropertyChain.

Two more remarks seem appropriate:

• We do allow range restrictions on reflexive and transitive roles, unless they are used in axioms following the forbidden pattern above
• EL++ inherits the acyclicity condition on complex property inclusions imposed by OWL 1.1 DL. However, in contrast to OWL 1.1 DL, this condition could in principle be dropped without losing decidability or tractability. Still, we should adopt that condition to be a real (syntactic) fragment.

Datatypes

I will be sketchy here since the datatype mechnism of OWL 1.1 DL is still in flux. The basic idea is that we have all datatypes of OWL 1.1 DL, but

• no DataComplementOf
• DataOneOf only with a single constant, but not with multiple ones
• very careful DatatypeRestrictions, if any. For example, we could allow MaxInclusive, but then not MinInclusive (and the other way round)
• DataSomeValuesFrom and DataHasValue, but no dataAllValuesFrom
• DataMaxCardinality and DataExactCardinality with cardinality 1, but for no other cardinalities
• no DataMinCardinality

Some Pointers to the Literature

EL++ was introduced in the conference paper [IJCAI05], though in a slightly different version than the one reported here (because, here, EL++ is tailored towards OWL 1.1 DL). The cited paper is accompanied by a technical report [TR05] containing more details. It contains a proof of tractability and also shows that EL++ is a maximal tractable fragment in the sense that, when standard expressive means such as inverse properties and cardinality restrictions are added, tractability is lost. How to efficiently implement the polytime algorithms from [IJCAI05] was studied in [M4M05]. The algorithms described in that paper underly the CEL reasoner. A system description of CEL is given in [IJCAR06].

Other research on EL++ and its variations has considered, for example, conjunctive query answering over instance data [DL07],[ISWC07],[LPAR07], explaining the results of classification [KI07], and deciding conservative extensions, which is related to the modularity of ontologies [CADE07].

References

[IJCAI05]

Pushing the EL Envelope. F. Baader, S. Brandt, and C. Lutz. In Proc. of the 19th Joint Int. Conf. on Artificial Intelligence (IJCAI 2005), 2005.

[TR05]

Pushing the EL Envelope. F. Baader, S. Brandt, and C. Lutz. LTCS-Report 05-01, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.

[M4M05]

Is Tractable Reasoning in Extensions of the Description Logic EL Useful in Practice?. F. Baader, C. Lutz, and B. Suntisrivaraporn. In Proceedings of the Methods for Modalities Workshop (M4M-05), Berlin, Germany, 2005.

[IJCAR06]

CEL—A Polynomial-time Reasoner for Life Science Ontologies. F. Baader, C. Lutz, and B. Suntisrivaraporn. In U. Furbach and N. Shankar, editors, Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), volume 4130 of Lecture Notes in Artificial Intelligence, pages 287–291. Springer-Verlag, 2006.

[ISWC07]

Conjunctive Queries for a Tractable Fragment of OWL 1.1. M. Kroetzsch, S. Rudolph, P. Hitzler. In K. Aberer and K.-S. Choi and N. Noy and D. Allemang and K.-I. Lee and L. Nixon and J. Golbeck and P. Mika and D. Maynard and R. Mizoguchi and G. Schreiber and P. Cudré-Mauroux, Proceedings of the 6th International Semantic Web Conference (ISWC 2007), volume 4825 of LNCS, pp. 310--323. Springer, November 2007.

[DL07]

On conjunctive query answering in EL. R. Rosati. In Proceedings of the 2007 International Workshop on Description Logic (DL 2007), CEUR Electronic Workshop Proceedings, 2007.

[LPAR07]

Data Complexity in the EL family of Description Logics. A. Krisnadhi and C. Lutz. In Proceedings of the 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR07), LNCS. Springer Verlag, 2007.

[KI07]

Pinpointing in the Description Logic EL+. F. Baader, R. Penaloza, and B. Suntisrivaraporn. In Proceedings of the 30th German Conference on Artificial Intelligence (KI2007), LNAI, Springer-Verlag, 2007.

[CADE07]

Conservative Extensions in the Lightweight Description Logic EL. C. Lutz and F. Wolter. In Proceedings of the 21st Conference on Automated Deduction (CADE-21). Springer-Verlag, 2007.