Modeling in OWL 2 without Restrictions
  The Semantic Web ontology language OWL 2 DL comes with a variety of language
features that enable sophisticated and practically useful modeling. However,
the use of these features has been severely restricted in order to retain
decidability of the language. For example, OWL 2 DL does not allow a property
to be both transitive and asymmetric, which would be desirable, e.g., for
representing an ancestor relation. In this paper, we argue that the so-called
global restrictions of OWL 2 DL preclude many useful forms of modeling, by
providing a catalog of basic modeling patterns that would be available in OWL 2
DL if the global restrictions were discarded. We then report on the results of
evaluating several state-of-the-art OWL 2 DL reasoners on problems that use
combinations of features in a way that the global restrictions are violated.
The systems turn out to rely heavily on the global restrictions and are thus
largely incapable of coping with the modeling patterns. Next we show how
off-the-shelf first-order logic theorem proving technology can be used to
perform reasoning in the OWL 2 direct semantics, the semantics that underlies
OWL 2 DL, but without requiring the global restrictions. Applying a naive
proof-of-concept implementation of this approach to the test problems was
successful in all cases. Based on our observations, we make suggestions for
future lines of research on expressive description logic-style OWL reasoning.
