From: Conrad Bock <conrad.bock@nist.gov>

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>

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. ConradReceived on Wednesday, 18 April 2007 14:56:38 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 20:58:15 UTC
*