Question re: HasKey entailments

(Since I'm not a member of the WG this can be considered a LC comment  
or since my group is in the group, you can consider it an internally  
discussible comment)

I was talking to someone about keys and we were looking at the  
document section on this (http://www.w3.org/2007/OWL/wiki/Syntax#Keys)  
where the example is given of

HasKey( a:Person a:hasSSN ) 	
PropertyAssertion( a:hasSSN a:Peter "123-45-6789" ) 	
ClassAssertion( a:Person a:Peter ) 	
PropertyAssertion( a:hasSSN a:Peter_Griffin "123-45-6789" ) 	
ClassAssertion( a:Person a:Peter_Griffin ) 	

and my colleague asked why the last axiom wasn't entailed by the  
HasKey.  We went and looked in the model theory, and it says under the  
circumstances of the first four expressions HasKey won't apply  
(because there's no evidence of a CE for Peter_Griffin) -- so it  
appears this is not entailed in the current model theory.
  Guess my question is why does one need the additional condition (and  
thus the additional axiom) -- wouldn't it follow that if HasKey  
relates person's via hasSSN (i.e. the HasKey assertion) that anything  
that has that key (the SSN) would have to be a person?
  If HasKey would entail that the domain of the property asserted  
would be the first argument to the HasKey (which is what seems to be  
intended) then wouldn't the fact that X is an element of
(CE)^^C [1] and in fact that it is a Person follow?
    Is there a reason we don't do this ?-- would seem to simplify the  
use of HasKey without causing an obvious semantic harm that I can see  
(and would make its use more intuitive in many cases).
    thanks
    JH




[1] sorry, my mailer doesn't seem to like the fonts from the document  
- see http://www.w3.org/2007/OWL/wiki/Syntax#Keys fpr the

Received on Monday, 29 December 2008 20:58:26 UTC