Re: TEST: FunctionalProperty InverseFunctionalProperty 3.4 4.1

On August 1, Jeremy Carroll writes:
> 
> 
> 
> Ian Horrocks wrote:
> 
> > On July 26, Jeremy Carroll writes:
> > I am also concerned about tests in the style of FunctionalProperty
> > test 003. Here, we are asked to conclude that a property is
> > InverseFunctional given that its inverse is functional. This is a
> > higher order inference that is a consequence of the semantics of OWL,
> > but cannot be proved within OWL. I.e., OWL does not state anything
> > like:
> > 
> > forall P,Q . FunctionalProperty(P) ^ inverse(P,Q) -> InverseFunctionalProperty(Q)
> > 
> > I would *NOT* expect an OWL reasoner to find this inference.
> > 
> 
> 
> 
> I could support this as a non-entailment test.
> 
> As soon as we have an interesting divergence of views it behoves
> to make up our minds and choose either an entailment test or
> a non-entailment test.
> 
> 
> i.e. instead of the comment:
> 
> <!--
>   If prop is an owl:FunctionalProperty,
>   then its inverse is an owl:InverseFunctionalProperty.
> -->
> 
> We could have the comment
> 
> <!--
>   If prop is an owl:FunctionalProperty,
>   then its inverse, while being constrained to be
>   consistent with being an owl:InverseFunctionalProperty
>   should not be deduced as being one.
> -->
> 
> 
> i.e. from
> 
> http://www.w3.org/2002/03owlt/FunctionalProperty/premises003.rdf
> 
> it does not follow that
> 
> http://www.w3.org/2002/03owlt/FunctionalProperty/conclusions003.rdf
> 
> 
> This would fit with my preferred reasoning style in which the statements
> such as
> 
> 
> :inv a owl:InverseFunctionalProperty .
> 
> are within the domain of discourse, and have semantic import over and above
> their definition, which is a necessary but not sufficient condition.
> 
> As far as I can see, the non-entailment test follows from a
> Connolly/solipsistic/DAML+OIL axiomatic style of semantics
> 
> whereas the entailment test reflects a Patel-Schneider view of the
> world in which the definition is a neecessary and sufficient condition.

This is wrong. The MT simply imposes a restriction that, in all
models, the interpretation of a TransitiveProperty must be closed
under transitivity. This does not mean that any property that is
closed under transitivity in all models is necessarily a
TransitiveProperty (such a situation could result from other causes,
e.g., the properties interpretation being empty in all models, or the
size of the domain being less than 3 in all models).

Ian



> 
> 
> Jeremy
> 
>

Received on Thursday, 1 August 2002 19:57:33 UTC