Re: Question on DL negation

On Mar 7, 2007, at 2:22 PM, Michael Schneider wrote:
[snip]
> Unluckily, I cannot check this with the navigator, because there is  
> no such "concept disjointness" checkbox. It seems that all I can do  
> is comparing the complexity classes of OWL-Lite and OWL-DL, which  
> is an upper-language of OWL-Lite+disj:
>
>    * Complexity( OWL-Lite )  = ExpTime (complete)
[snip]

It stays EXPTIME-complete since you can polynomially encode class  
disjointness in OWL-Lite. I was going to gin up an example using min1  
and max0 on some dummy property, but the I found it in an email:
	<http://lists.w3.org/Archives/Public/www-webont-wg/2003Jun/0259>

(At the bottom.)

""" > > [1] An example construct, which Jeremy credits to Ian  
Horrocks, is as follows.
 > > >
 > > > Given a definition of a class C:
 > > >    Class(C complete <expr1>)
 > > >
 > > > The let P be a property which is not used elsewhere and define:
 > > >    Class(C complete restriction(minCardinality(P, 1))
 > > >    Class(C-co complete restriction(maxCardinality(P, 0))"""

(Er..it would have been less work to just recreate it, but I was  
looking for a better overall explanation)

Cheers,
Bijan.