RE: Inferring Properties based on Types

Hello again, Ian!

You are (and were) right, and I were wrong! :-(

Ian Horrocks wrote:

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

No, you did not confuse me, neither by using "ObjectExists", nor by reusing
the name "manman". Look what I wrote in my previous mail:

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

I really had understood your "ObjectExists" as a "SomeValuesFrom" axiom, and
I had myself substituted "manman" by "r". So I cannot use this as an excuse.
The fact is that I simply did not see your argument!  

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

Yes. Your first axiom 

  (1) SubClassOf(Man objectSomeValuesFrom(manman Thing))

only demands that IF it can be entailed that "y IN Man", THEN there has to
be some property instance "manman(y,z)" (for some z). But IF "y IN Man"
CANNOT be entailed, THEN it is irrelevant if there is such a "manman(y,z)"
property instance. In such a case I can, for example, choose some model M,
where the *empty* property "owl:Nothing X owl:Nothing" is denoted by
"manman". This really does not contradict the first axiom. But with this
empty "manman" property, it is clear that your second axiom

  (2) SubObjectPropertyOf(
        SubObjectPropertyChain(sibling manman
          InverseObjectProperty(manman)) 
        brother)    

cannot be used anymore to entail "brother(x,y)", because in the equivalent
form:

  (2')  FORALL a,b,c,d: sibling(a,b) AND manman(b,c) AND manman^-1(c,d) ==>
brother(a,d)

(I use "manman^-1" here to denote the inverse property of "manman") or
respectively:

  (2'') FORALL a,b,c,d: sibling(a,b) AND manman(b,c) AND manman(d,c) ==>
brother(a,d)

there will be of course no chance to have any match for the two
"manman(.,.)" terms on the left hand side of this rule expression.

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

Yes. Having "sibling(x,y)" and "Man(y)" gives me "EXISTS z: manman(y,z)"
from your first axiom (1). And now I can choose in the rewritten form (2'')
of the second axiom:

  a := x
  b := y
  c := z
  d := y

And, woops, I receive "brother(a,d)" = "brother(x,y)".

Great! So we finally have received a not too complicated translation of
Tim's rule into OWL-1.1. Very nice! :)

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 13:21:37 UTC