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 Sunday, 7 October 2007 10:14:23 UTC