Adding a projection operator to OWL -?

Dear OWL experts,

does anyone know, if that would be possible to add the role projection 
operation to OWL 2, retaining the decidability and the possibility to 
use the role itself and its projection in the cardinality and role 
disjointness assertions?

If the role is t (for 'takes') and S (for 'Student') is a class name, 
one defines the projected role t@S to consist of those pairs (x,y), 
where both (x,y) \in t and x \in S.

There is a construction for role projection using a new S_self role such 
that (in informal notation):

Domain(S_self,S)
S = HasSelf(S_self)
S <= MaxCardinality(1,S,Thing)
SubProperty(t@S,t)
SubProperty(S_self o t, t@S)

However, in the presence of these axioms neither t nor t@S would be 
simple roles due to the property chain axiom for t@S, so the cardinality 
and role disjointness assertions for them would not be allowed in OWL 2.

The very first intuition would be that it should be possible to extend 
the decidability proof to include this construct, however, this does not 
seem to be a simple endeavour without deep DL expertise.

May be someone has already done this? Or can there be other ways solving 
the problem?

Thanks a lot in advance!

Kārlis Čerāns
Institute of Mathematics and Computer Science,
University of Latvia

Received on Friday, 17 March 2017 17:19:14 UTC