RE: OWL DL extension question

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.

Conrad

Received on Wednesday, 18 April 2007 14:56:38 UTC