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

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

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

> -Alan

peter

Received on Tuesday, 6 November 2007 18:03:49 UTC