Re: Inferring Properties based on Types

On 7 Oct 2007, at 11:14, Michael Schneider wrote:

> 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.

Perhaps I confused you by re-using the manman role name (or by using  
objectExists whan I meant objectSomeValuesFrom -- see below); in fact  
I could have used any role name that doesn't otherwise occur in the  
ontology/knowledge-base. It is true that when used in this way the  
manman role can take many different shapes, but this doesn't matter  
for our purpose (making sure that Tim's rule holds), because such  
"unintended" shapes will not hold in *every* model. I.e., for any two  
individuals x,y such that the ontology does not entail Man(y), there  
is *some* model of the ontology in which there is no z such that  
manman(y,z) holds, and thus brother(x,y) will not be entailed as a  
result of the property chain inclusion axiom. In contrast, if the  
ontology entails both sibling(x,y) and Man(y), then the additional  
axioms will ensure that it also entails brother(x,y). This is all we  
need. What you seem to be trying to achieve is to extend the ontology  
so that it entails Man(x) <=> manman(x,x). This might be interesting  
in itself, but is more than is needed in order to realise Tim's rule.



> 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)

What I meant here was, of course:

SubClassOf(Man objectSomeValuesFrom(manman Thing))
SubObjectPropertyOf(SubObjectPropertyChain(sibling manman  
InverseObjectProperty(manman)) brother)

Regards,
Ian




>
> 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 Tuesday, 9 October 2007 10:45:27 UTC