Re: Punning and the "properties for classes" use case (from public-owl-dev)

On 6 Nov 2007, at 17:49, Peter F. Patel-Schneider wrote:

> From: Alan Ruttenberg <alanruttenberg@gmail.com>
> Subject: Re: Punning and the "properties for classes" use case  
> (from public-owl-dev)
> Date: Tue, 6 Nov 2007 12:39:34 -0500
>
>> On Nov 6, 2007, at 5:14 AM, Peter F. Patel-Schneider wrote:
>>
>>>> But why couldn't we, with punning, for instance, have Class(C)  
>>>> entail
>>>> Individual(C) to more closely match the OWL Full case? Then we too
>>>> would have a domain size of 1 be inconsistent (because of the
>>>> presence of the individuals owl:Thing and owl:Nothing)?
>>>
>>> But nothing says that these two individuals are different.
>>
>> They have different size extensions. Isn't that enough? If they were
>> the same they would have to have the same extensions.
>
> Not enough if you have punning.  Remember that having the individual
> denoted by owl:Thing being the same as the individual denoted by
> owl:Nothing does not imply that their denotations as classes are
> equivalent.
>
> A slogan for punning:
> 	The sizes of the class are not visited on the individual.    :-)

I find it useful to think of punning as if there were a syntactic pre- 
processing step that prepends INDIVIDUAL- and PROPERTY- to all  
individual and property names (as determined by the context in which  
they are used). When you look at it this way, it is easy to see that  
owl:INDIVIDUAL-Thing has no special status w.r.t. owl:Thing -- it is  
just like any other individual name.


>
>>>> Wouldn't the entailments match in that case? - both would be
>>>> inconsistent, and hence both would entail anything.
>>>
>>> Nope.  You can't even get away in general by using unique names
>>> assumption to pump up the size of the domain.  OWL Full has only
>>> infinite domains (because its domains contain lots of bits of  
>>> syntax),
>>> and this has observable consequences.  For example, a spy point
>>> ontology
>>> that restricts the domain to maximum size 1 000 000 is  
>>> satisfiable in
>>> OWL DL but not in OWL Full.
>>
>> Is there an easy way to show this (for my collection of OWL  
>> examples?)
>
> You mean prove it?  OWL Full domains must be infinite, OWL DL domains
> don't have to be.  Both bits are easy to prove.
>
> You mean an ontology that is satisfiable in OWL DL but not in OWL  
> Full?
> The same example as before with 1 replaced by 1 000 000, i.e.,
>
> 	owl:Thing <= hasValue ( ex:r ex:spy )
> 	ex:r inverseOf ex:rinv
> 	ex:spy in atmost(1 000 000 ex:rinv)
>
>>>> In order to do this, we would need to, effectively, assert an
>>>> individual of the same name as  each entity(class or property)  
>>>> in the
>>>> ontology. While I can imagine why this might be considered
>>>> distasteful, would it work from a technical point of view as far as
>>>> getting us closer to OWL Full alignment?
>>>
>>> No.
>>
>> OK. Follows from the fact that Full domains are infinite.
>>
>> What about going the other way? Jeremy mentioned that David Turner
>> proposed some axioms that, if I understood things correctly, would
>> assert owl:Thing to be infinite even in the DL case. (he'll send a
>> followup email with the details). This may not be desirable from the
>> point of view of wanting DL to be able to be finite to enable certain
>> types of computation, like some approximations of closed-world-
>> reasoning, but I want to separate that out and understand the
>> technical issues, if you will help me.
>
> Axioms?  You mean something like
>
> 	ex:pred inverseOf ex:succ
> 	ex:SP = exactly( 1 ex:succ ) and exactly( 1 ex:pred ) and all 
> ( ex:succ SP )
> 	ex:zero in exactly ( 1 ex:succ ) and exactly ( 0 ex:pred ) and all  
> ( ex:succ SP )
>
> This forces the domain to infinite, but why would you ever want to
> enforce that these axioms are true in all OWL DL ontologies?

I guess that Alan wants to rule out the finite domain "corner cases"  
that lead to differences between OWL DL and OWL Full. I'm not sure  
how this helps.

Ian


>
>> -Alan
>
> peter

Received on Sunday, 11 November 2007 17:16:53 UTC