Complexity and implementability of OWL languages

As per action on me from the last telecon, here is a summary of the
known theoretical complexity results and practical implementability
results for the the various OWL languages.

OWL Lite

This language is completely contained in the SHIQ(D+) description
logic (or, if you prefer, in a decidable fragment of FOL defined by
the SHIQ(D+) description logic). From SHIQ(D+) we get an ExpTime upper
bound on the complexity of the satisfiability/subsumption problem and,
given that the same problems for ALC (a logic that is contained in OWL
Lite) are also in ExpTime, this is in fact a tight bound.

There are know "practical" algorithms for SHIQ(D+), i.e., algorithms
that carry out a goal directed search of the solution space, and that
can determine when they have fully explored the solution
space. Moreover, optimised implementations of SHIQ already exist, and
are currently being extended with datatype reasoning (some simple
datatype reasoning is already available in the RACER system). These
implementations have been shown to work reasonably well with realistic
problems, i.e., complex ontologies with thousands of classes, or
simpler ontologies with up to 100,000 classes.


OWL DL

This language is equivalent to the SHOIQ(D+) DL, i.e., SHIQ(D+)
extended with an equivalent of the oneOf constructor. As I have
mentioned in several earlier emails, the interaction of oneOf and
inverse roles pushes the complexity of the standard decision problems
into NExpTime. Again this is a tight bound, because the language has
been shown to be contained in C2 (the two variable fragment of FOL
with counting quantifiers), which is also in NExpTime (with unary
encoding of numbers). See [1] for more details about these results. Of
course the same result shows that the language is decidable.

Unfortunately, there are no know "practical" algorithms for SHOIQ(D+)
- it would probably be possible to create some sort of implementation
of C2 from the decidability/complexity proofs, but this would not have
the "nice" properties I mentioned above, and would be unlikely to be
useful in practice (no one has bothered to build such an
implementation up until now).

Having said that, as already mentioned, we do have effective
algorithms and implementations for the language without oneOf, and we
also have a goal directed (but as yet unimplemented) algorithm for the
language without inverse. Research is continuing to try to find a
suitable algorithm (possibly using automata techniques) for the full
language.


OWL full

It is easy to show that it is undecidable, as simply removing the
constraint on the use of transitive properties in cardinality
restrictions is enough to make it undecidable (see [2]). It should be
possible to embed the language in conventional FOL in such a way that
standard FOL provers can be used as sound but incomplete reasoners.



[1] ftp://www-lti.informatik.rwth-aachen.de/pub/papers/2001/Tobies-PhD-2001.pdf
[2] http://www.cs.man.ac.uk/~horrocks/Publications/download/2001/ijcai01.pdf

Received on Thursday, 19 December 2002 10:15:51 UTC