W3C home > Mailing lists > Public > public-owl-dev@w3.org > April to June 2007

RE: OWL DL extension question

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>
Message-ID: <016501c78122$ddcded40$b3200681@MEL.NIST.GOV>

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 GMT

This archive was generated by hypermail 2.3.1 : Wednesday, 27 March 2013 09:32:54 GMT