# RE: OWL DL extension question

Date: Wed, 18 Apr 2007 10:56:36 -0400
To: "'Yevgeny Kazakov'" <ykazakov@cs.man.ac.uk>
Cc: "'Ian Horrocks'" <horrocks@cs.man.ac.uk>, "'Evren Sirin'" <evren@clarkparsia.com>, "'Owl Dev'" <public-owl-dev@w3.org>, "'Evan Wallace'" <evan.wallace@nist.gov>, "'Nenad Krdzavac'" <nenad.krdzavac@gmail.com>
Message-ID: <01b201c781c9\$c31659e0\$b3200681@MEL.NIST.GOV>
```
Yevgeny,

>  Sorry, I have made some mistake in my previous post (swapped the
>  roles in compositions), the correct axioms C1--C4 should be as
>  follows:
>
>  C1. parent o brother => parent ( x is a parent of y and y
>  is a brother of z implies x is a parent of z)

>  C2. brother o parent => uncle  ( x is a brother of y and y
>  is a parent
>  of z implies x is an uncle of z)
>
>  when substituting parent from C1 into C2 we obtain:
>
>  brother o ( parent o brother ) => uncle
>
>  or
>
>  brother o parent o brother => uncle

I understood what you meant, thanks for updating my example.

>  the last property suggests that there is a relation R such that
>
>  brother o parent => R ( x is a brother of y and y is a parent of z
>  then x is an R of z )
>  and
>  R o brother => uncle ( x is an R of y and y is a brother of z then x
>  is an uncle of z )
>
>  naturally,  R = uncle :
>
>  C3. brother o parent => uncle
>  C4. uncle o brother  => uncle

Yes, though of course R isn't equivalent to (=) uncle, it's a subclass
of uncle.

>  Let me correct your axioms in a similar way and introduce
>  names for them:
>
>  A1 brother o parent => uncle ( if x is a brother of y and y is a
>  parent of z then x is an uncle of z )

>  A2 uncle o child => brother ( if x is an uncle of y and y is a child
>  of z then x is an brother of z )

>  >   (where we assume
>  >
>  >        - child = inverse of parent (following Evren's suggestion)
>  >        - a child has exactly one parent (can give more realistic
>  >            examples later)
>  >
>  >    The intention is to specify uncles exactly, rather than only a
>  >    superset or subset.
>  >   )

>  I don't think this is sufficient to specify uncles exactly: it is
>  still possible to have (x is an uncle of z) without having y such
>  that ( x is a brother of y ) and ( y is a parent of z).

If we assume parent (=Inv(child)) is functional (a number restriction
being OK here, because child and parent are simple), and it's domain
isn't restricted, then if (x is an uncle of z), z will be the child of
some y, whereupon by A2, x is a brother of y.  Did I get that right?

> In general, specifying a role *exactly* as composition of other
> roles, e.g.

>  R o S = T
>  that is:
>  R o S => T ( x R y and y R z implies x T z )
>  *and*
>  T => R o S ( x T z implies *there exits* y such that x R y
>  and y S z )

>  easily leads to undecidability already for ALC (this allows one to
>  express that the diagonal of a grid is exactly the composition of
>  the horizontal and vertical relations, which gives a reduction for
>  undecidability).

OK, however, T => R o S is outside the role inclusions allowed in SROIQ,
whereas A1 and A2 are inside.

>  > [Conrad] Wasn't sure how to apply your looser restrictions to
>  > inclusions with less than three properties in the premise, so I
>  > tried substituting each inclusion into the other:
>  [Yevgeny] correcting (was my fault):
>
>  A2=>A1: ( uncle o child ) o parent => uncle
>  A1=>A2: ( brother o parent ) o child => brother

>  > [Conrad] Changing the associativity:
>  [Yevgeny] correcting:
>
>  uncle o ( child o parent ) => uncle
>  brother o ( parent  o child ) => brother

>  > These are both true (the second assuming one parent per child).
>  > Is your looser restriction is satisfied?

>  Not yet :-)

>  The restriction say that the axioms should not only be true, but
>  provable in any order. In particular, for the first axiom [snip],
>  one needs to introduce this role explicitly and add the missing
>  axioms:

Thanks for working out the additional axioms and critical pairs.  Does
this mean A1 and A2 satisfy your looser regularity restrictions?

>  The restrictions allow one to detect missing relations and axioms.
>  E.g. the critical pair between A1 and A2:
>
>  A1=>A2: ( brother o parent ) o child => brother
>  yields: brother o ( parent o child ) => brother
>
>  The critical pair indicates that there is an implicit relation
>  R for the composition ( parent o child ) which enjoys the
>  properties:
>
>  parent o child => R,  and
>  brother o R => brother

>  the expert can look at these axioms and see what R could be (in our
>  case it was easy to guess that R = "have_common_parents").  In many
>  cases the missing relations are obvious, like it was in our example.
>  It is counterintuitive to have R o S o T => H to be provable only
>  from "left-to-right" or "right-to-left" for the relations from the
>  "physical world", as composition in "physical world" is always
>  associative (parenthesis do not matter).

Not sure I would call the above axioms "missing", since, as you say,
they are implict in A1 and A2.  I assume they are only needed for
restriction-checking, not for DL reasoning, is that right?

>  >  > [Yevgeny] Regarding maximality, *I do not have a proof yet*,
>  >  > but I conjecture that any system of compositional role axiom
>  >  > that is not regular, gives undecidability. That is, if we *fix*
>  >  > a set of these axiom RBox and consider *arbitrary* (ALCI)
>  >  > TBoxes, then the subsumption w.r.t.  (varying) TBox + (fixed)
>  >  > RBox is probably undecidable.

>  > [Conrad] That would be very interesting.  This wouldn't preclude
>  > the existence of other maximal restrictions, however, right?

>  [Yevgeny] well yes and no.

>  No (that is it would preclude in a certain sense) because I think
>  y set of *regular* compositional axioms can be extended with fresh
>  role names and new compositional axioms with them such that all the
>  necessary conditions are satisfied.  This is not possible, however,
>  for the restrictions in SROIQ.  That is, the restriction is powerful
>  enough to capture all the regular compositional axioms (and as I
>  conjecture, this is maximal one can achieve in the sense above) Also
>  my restrictions is not exactly "looser" than those in SROIQ. In
>  fact, for the SROQ RBoxes my restrictions do not hold. But it is
>  possible to convert any SROIQ TBox **automatically** into the one
>  where restrictions hold by introducing the required roles and axioms
>  for the critical pairs.  That is, in case the ontology engineer is
>  too lazy to resolve all critical pairs, one can employ the "lighter"
>  restrictions from SROIQ.

>  Yes, because there might be other restrictions which are also
>  powerful enough to capture all regular compositional axioms.

And there might be other restrictions besides regularity that are also
maximal.