# RE: OWL DL extension question

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.