Re: OWL DL extension question

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