RE: Inferring Properties based on Types

Michael, Evren, Dmitri, Ian,

Wow. I've been away for about over a week now, and I just read this entire thread at once, starting with http://lists.w3.org/Archives/Public/public-owl-dev/2007JulSep/0212.html. My head is still spinning.

The feedback is interesting, and I will have to re-read the posts to grock the complete logical consequences of these axioms, but it's encouraging to know that this can be done. Thanks for the responses. I was vaguely aware of, but not very familiar with, self restrictions and reflexive properties in OWL 1.1. I will have to read up on that too.

It bothers me that I'm busy with another project right now and won't have any time to give over to experimenting with this. I get back from out of town next week, and I'll try to find some time to take a look at it. I'll surely post here if I come up with any questions.


Thanks for the fascinating discussion,

Tim Swanson
Semantic Arts, Inc.
Fort Collins, Colorado


> -----Original Message-----
> From: Michael Schneider [mailto:schneid@fzi.de]
> Sent: Sunday, October 07, 2007 4:14 AM
> To: Ian Horrocks
> Cc: Owl Dev; Evren Sirin; Swanson, Tim
> Subject: RE: Inferring Properties based on Types
> 
> Hi, Ian!
> 
> Ian Horrocks wrote:
> 
> >Thanks for pointing out my error in asserting that it wasn't possible
> >to express Tim's rule in OWL 1.1.
> >
> >Now you have pointed out the basic trick, I wonder why the set of
> >axioms for expressing this rule is so complex. In particular, why do
> >we need it to be the case that manman(x,x) <=> Man(x) -- wouldn't it
> >be enough that Man(x) => manman(x,x)?
> 
> I think this condition would be too weak, because it would allow the
> 'manman' role to take many different shapes without hurting this
> condition.
> For example, the /identity/ relationship id(x,x) :<=> x=x would be
> allowed
> for the 'manman' role by such a condition. And more generally, every
> role
> which is reflexive would also be allowed, so for instance the "full"
> role
> "owl:Thing X owl:Thing" could then be used as the 'manman' role. This
> would
> have the potential of introducing problems, I believe.
> 
> >We could also do without
> >reflexivity -- we could simply use an existential restriction to
> >force the existence of *some* manman relation and then use (sibling
> >manman InverseObjectProperty(manman)) as the role chain implying
> >brother. This would give:
> >
> >SubClassOf(Man ObjectExists(manman Thing))
> >SubObjectPropertyOf(SubObjectPropertyChain(sibling manman
> >InverseObjectProperty(manman)) brother)
> 
> The first axiom here will be consistent with any model that uses for
> 'manman' a role r, which for each Man x ensures the existence of some
> instance y so that r(x,y) holds. For example, manman := id would be a
> permitted role by this first axiom, because id(x,x) holds for every
> instance
> x, so especially it holds for each Man x, and by setting y := x we get
> the
> existence of some instance y with id(x,y). Hence, for each Man x there
> is
> some instance y with manman(x,y). But by choosing the identity
> relationship
> as the 'manman' role, we can do the following inference starting from
> the
> second axiom:
> 
>   SubObjectPropertyOf(SubObjectPropertyChain(
>     sibling manman InverseObjectProperty(manman)) brother)
> 
>   |= SubObjectPropertyOf(SubObjectPropertyChain(
>        sibling id InverseObjectProperty(id)) brother)
> 
>   |= SubObjectPropertyOf(SubObjectPropertyChain(
>        sibling id)) brother)
> 
>   |= SubObjectPropertyOf(sibling brother)
> 
> And this is certainly not what we intended to get, because suddenly
> every
> sibling is a brother, without needing to check if it also is a Man. And
> when
> we select for instance manman := "owl:Thing X owl:Thing", which is also
> allowed by the first axiom above, then we may even get more unintended
> brothers.
> 
> Note that with my original two conditions
> 
>   FORALL x: Man(x) <=> manman(x,x)
>   FORALL x,y: manman(x,y) => x=y
> 
> the situation "manman = id" can also occur, but only with models for
> which
> Man = owl:Thing. And in *this* specific case it is really true that
> every
> sibling is also a brother. But I tried to choose my two conditions in a
> way,
> which allows me to deal with *every* case, i.e. with models having
> arbitrary
> extensions of class Man. I did this by trying to specify my 'manman'
> role in
> the most restrictive way which I could think of, so that unintended
> interpretations for 'manman' are not possible.
> 
> At least, it seems that I can show that under my two conditions, the
> 'manman' role is /uniquely/ specified with respect to a given model:
> Let
> 'manman1' and 'manman2' be two roles for which the above two conditions
> hold. Let's start with two arbitrary instances x and y, for which
> manman1(x,y) is true. Then from the second condition we receive x=y, so
> manman1(x,x) is true. From the first condition we then get Man(x). And
> because 'manman2' also matches the two conditions, we get manman2(x,x)
> from
> the first condition. But we had x=y, so finally manman2(x,y) is true.
> The
> other direction of this equality proof is performed analog.
> 
> Cheers,
> Michael
> 
> --
> Dipl.-Inform. Michael Schneider
> FZI Forschungszentrum Informatik Karlsruhe
> Abtl. Information Process Engineering (IPE)
> Tel  : +49-721-9654-726
> Fax  : +49-721-9654-727
> Email: Michael.Schneider@fzi.de
> Web  : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555
> 
> FZI Forschungszentrum Informatik an der Universität Karlsruhe
> Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
> Tel.: +49-721-9654-0, Fax: +49-721-9654-959
> Stiftung des bürgerlichen Rechts
> Az: 14-0563.1 Regierungspräsidium Karlsruhe
> Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi Studer
> Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus

Received on Monday, 8 October 2007 16:58:17 UTC