- From: Yevgeny Kazakov <ykazakov@cs.man.ac.uk>
- Date: Tue, 17 Apr 2007 23:46:34 +0100
- To: conrad.bock@nist.gov
- 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>
Hi Conrad and others, 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 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 On 4/17/07, Conrad Bock <conrad.bock@nist.gov> wrote: > > Thanks. Just to make sure I understand, would the following be a case > where the looser restrictions allow axioms the SROIQ restrictions don't: > > parent o brother => uncle > > child o uncle => brother 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) One should be careful with counting restrictions on roles that can appear in compositional axioms. Generally, the counting restrictions on non-simple roles---namely on those that can be implied (directly or indirectly) by composition of other roles---cause problems with decidability (it is probably pointed out in the SROIQ paper). In axioms A1 and A2 the role parent (= inverse of child) is simple since it does not appear in the right-hand-side of the implications, hence it can be asserted to be functional. However, say, when we add axiom C1 it is no longer simple as both parent and child can be implied by composition of other roles (from C1). > 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). 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). > My understanding is the above would be irregular under the SROIQ > restrictions, because uncle and brother appear on both sides of the > inclusions, creating a circularity. correct. the restrictions for SROIQ imply from A1 that brother > uncle and from A2 that uncle > brother which causes a loop. > 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: > > parent o (child o uncle) => uncle > > child o (parent o brother) => brother correcting (was my fault): A2=>A1: ( uncle o child ) o parent => uncle A1=>A2: ( brother o parent ) o child => brother > Changing the associativity: > > (parent o child) o uncle => uncle > > (child o parent) o brother => brother 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 there should be a role R for ( child o parent ), that is: child o parent => R ( x is a child of y and y is a parent of z implies x is an R of z ) and uncle o R => uncle ( x is an uncle of y and y is an R of z implies x is an uncle of z ) clearly, in this case x R y should mean that "x and y have common parents" (e.g. x = y or x is a brother of y or x is a sister of y ). Hence, in order to fulfill the requirements, one needs to introduce this role explicitly and add the missing axioms: A3 child o parent => common_parents A4 uncle o common_parents => uncle similarly for the second axiom brother o ( parent o child ) => brother there should be a role S for ( parent o child ) such that parent o child => S and brother o S => brother well, in case if we assume a parent is unique, then S should be just an identity relation also known as a "self" relation ( x self y implies x=y), (however this might be problematic for decidability since self must have other properties like self o parent => parent, and so parent is no longer a simple role. In fact this property will be derived.) that is, we need to add axioms : A5 parent o child => self A6 brother o self => brother Now also A4 can be substituted into A2 and A6 can be substituted into A1 creating new "critical pairs" (this is a terminology from term rewriting): A4=>A2: ( uncle o common_parents ) o child => brother A6=>A1: ( brother o self ) o parent => uncle again, if we shift the parenthesis we get: uncle o ( common_parents o child ) => brother brother o ( self o parent ) => uncle which requires new roles for the composition in parenthesis. Luckily, no new roles are needed: the first is will be clearly child, the second is parent: A7 common_parents o child => child (axiom uncle o child => brother is already there: A2 ) A8 self o parent => parent (axiom brother o parent => uncle is already there: A1 ) commuting the parenthesis we obtain: uncle o ( common_parents o child ) => brother parent o ( self o parent ) => uncle Moreover, A4 and A8 make critical pairs with themselves: A4=>A4: ( uncle o common_parents ) o common_parents => uncle A8=>A8: self o ( self o parent ) => parent which should be resolved: uncle o ( common_parents o common_parents ) => uncle ( self o self ) o parent => parent luckily again we can just set common_parents and self to be transitive: A9 common_parents o common_parents => common_parents A10 self o self => self Some more: A5=>A8: ( parent o child ) o parent => parent parent o ( child o parent ) => parent by A3 we have child o parent => common_parent, so we need to add: A11 parent o common_parents => parent A5=>A10: ( parent o child ) o self => self parent o ( child o self ) => self we add: A12 child o self => child So now, if I did not miss anything the set of axioms is complete, that is, all the critical pairs are resolved: A1 brother o parent => uncle A2 uncle o child => brother A3 child o parent => common_parents A4 uncle o common_parents => uncle A5 parent o child => self A6 brother o self => brother A7 common_parents o child => child A8 self o parent => parent A9 common_parents o common_parents => common_parents A10 self o self => self A11 parent o common_parents => parent A12 child o self => child > What is the definition of a commuting pair of composition axioms? OK, formally the definition for the sufficient conditions is the following: Let RBox be a set of role axioms of form R => S (usual role hierarchies) or R o S => T (compositional axioms) where R and S are arbitrary roles (possibly inverses). We say that RBox is complete (or associative for compositions) if whenever R o S => T is "provable" from the RBox and T o H => V is "provable" from the RBox that is, (R o S) o H => V is provable from the RBox then R o (S o H) => V should also be provable from the RBox that is, there exists a role U for ( S o H ) such that: S o H => U is "provable" from the RBox and R o U => V is "provable" from the RBox Here R o S => T is "provable" from the RBox means that either: R1 o S1 => T1 is in RBox for some super-role R1 of R, super-role S1 of S and sub-role T1 of T (I assume the role is also a sub-role and a super-role of itself) or iS1 o iR1 => iT1 is in RBox for some inversed super-role iS1 of S1, inversed super-role iR1 of R1 and inverse sub-role iT1 of T1. > > In particular, it allows one to detect modeling errors: for example > > if there are only compositional axioms C1 and C2 in an ontology but > > not C3 and C4, the ontology is clearly underspecified, and this will > > be detected by the associativity test: there is a "left-to-right" > > proof for "brother o parent o brother => uncle", but no > > "right-to-left" proof. Another argument for this condition is that > > for most roles that come from "physical relations", the chains of > > roles should be composable regardless the direction. > > Didn't follow how the looser restrictions tell you when the ontology is > underspecified. Wouldn't only the subject matter expert know that? 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). > > 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. > > That would be very interesting. This wouldn't preclude the existence of > other maximal restrictions, however, right? well yes and no. No (that is it would preclude in a certain sense) because I think any 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. > > I would be interested if anyone would provide examples of such > > compositional properties that can be of interest in ontologies. > > We have many examples, can discuss off list. Sure, I will be more than happy to see some useful examples. I guess you have my email address. regards, Yevgeny Kazakov
Received on Wednesday, 18 April 2007 15:46:13 UTC