RE: OWL DL extension question

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