- From: Conrad Bock <conrad.bock@nist.gov>
- Date: Tue, 17 Apr 2007 15:01:53 -0400
- To: "'Yevgeny Kazakov'" <ykazakov@cs.man.ac.uk>, "'Ian Horrocks'" <horrocks@cs.man.ac.uk>
- Cc: "'Evren Sirin'" <evren@clarkparsia.com>, "'Owl Dev'" <public-owl-dev@w3.org>, "'Evan Wallace'" <evan.wallace@nist.gov>, "'Nenad Krdzavac'" <nenad.krdzavac@gmail.com>
Yevgeny, > I came up with a different restriction based on the property of > associativity. To illustrate, consider an axiom: 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 (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. ) 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. 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 Changing the associativity: (parent o child) o uncle => uncle (child o parent) o brother => brother These are both true (the second assuming one parent per child). Is your looser restriction is satisfied? > C1. brother o parent => parent ( a parent of my brother is > my parent ) > C2. parent o brother => uncle ( a brother of my parent is > my uncle ) > It is relatively easy to check whether this associativity condition > holds by checking whether all "critical pairs" between compositional > axioms commute ( C1 and C2 form a critical pair because the result > of C1 can be substituted into the premise of C2 ). What is the definition of a commuting pair of composition axioms? > C3. parent o brother => uncle ( a brother of my parent is > my uncle ) > C4. brother o uncle => uncle ( an uncle of my brother is my uncle ) > 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? > 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? > 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. Conrad
Received on Tuesday, 17 April 2007 19:02:39 UTC