Re: Question on DL negation

Hi Bijan, Evgeny and Ulrike!

I got a lot of input by you. Many thanks! I will answer (well, it's more
of a summary) all of them in this single mail.

Ulrike Sattler wrote at 5 Mar 2007 15:38:

> Michael Schneider wrote:
>> So, what's missing (at least from the perspective of role negation)  
>> in the current OWL11 draft are logical constructors for properties:  
>> 'unionPropertyOf', 'intersectionPropertyOf' and  
>> 'complementPropertyOf' - and perhaps syntactic sugar like  
>> 'DisjointPropertyUnion'.
>>
>> But I'm most probably not the first one who stumbles over this, so  
>> there might be at least two reasons, why there are no such  
>> constructors:
>>
>>   1) Very few interest or usecases on them, and/or
>>
>>   2) perhaps they would even break decidability of OWL/DL.
> 
> Hi Michael, it does not necessarily break it, but it might make it  
> very much harder because it is "un-local", and locality is a property  
> that all known reasoning & optimisation techniques make use of. If  
> you want to know more, have a look at "Mary likes all cats" (ie,  
> whomever Mary does not like is not a cat, i.e., this is an  
> allValuesFrom on a role complement) at
> 
> C. Lutz and U. Sattler. Mary likes all Cats. In F. Baader and U.  
> Sattler, editors, Proceedings of the 2000 International Workshop in  
> Description Logics (DL2000), number 33 in CEUR-WS, pages 213-226,  
> Aachen, Germany, August 2000. RWTH Aachen. Proceedings online  
> available from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/ 
> CEUR-WS/Vol-33/.
> Bibtex entry Abstract Paper
> 
> Cheers, Uli

[So this probably was the mail which Bijan referred to in his first answer.]

While I do not understand the meaning of "locality" in this context (but
I could probably read about it in the cited literature, thanks for the
link!), at least I see, why those role constructors did not make their
way into the OWL1.1 proposal, even if "OWL1.1+role constructors" turns
out to be decidable some day: According to [1], all new features of
OWL1.1 must

   "have effective reasoning methods, as evidenced by theoretical
   results"

And as long as this is not the case for the role constructors (and, if I
correctly understand you, it is unlikely that this will happen in the
near future), they keep out of the language. Good!


Evgeny Zolin ezolin@cs.man.ac.uk wrote on 7 Mar 2007 (offlist):

> Michael Schneider wrote:
>> > BTW1: Why is the complexity classification for the combination  
>> > "OWL1.1 plus role constructors" more specific ("NExpTime-hard")  
>> > than for OWL1.1 alone (just "decidable")?
> 
> "NExpTime-hard" is NOT more specific than "decidable".
> The former is a lower bound, the latter is an upper bound.
> So it's not a bug, and the DL Navigator says exactly what we (or at least I) know:

Ok, sorry, I meant something else, but it doesn't matter anymore. I now
see that "<COMPLEXITYCLASS>-hard" is meant to include undecidability.
That sounds reasonable to me, when I imagine an undecidable problem to
have "infinite" complexity. I was yet accustomed, though, to never talk
about the complexity class of a problem, as long as its decidability has
not yet been proofed. But that is probably a little to rigorous in practice.

But, in the case that I am not the only one who is puzzled by this:
Would you mind to add a note on this in the list of notes?

> OWL 1.1 is decidable (in fact, at least NExpTime-hard, and the upper bound is unknown),
> but the effect of adding those 3 mentioned role constructors (role complement,
> intersection, and union) to OWL 1.1 is unknown (at least to me), so it's lower bound is
> again "NExpTime-hard".

Perhaps a little more information should be added to the result table,
to distinguish the following results:

    * NExpTime-hard, possibly undecidable (as for OWL1.1 + constructors)
    * NexpTime-hard, proofed as decidable (as for OWL1.1)

Currently, when I want to get a lower bound for OWL1.1, I have to get
the result for OWL-DL (NExpTime-complete) to infer that OWL1.1 (as an 
upper language to OWL-DL) is NExpTime-hard. A little inconvenient. (But 
ok, it's of course good for learning to use the tool :) ).

> PS. I've heard (from Uli?) that adding those 3 role constructors to OWL (i.e., SHOIQ) has
> no effect on the complexity (i.e., it is still NExpTime-complete), but I have no reference
> to the result (so DL Navigator shows only hardness here). For OWL 1.1, I have not heard
> any rumours on the same issue at all.

Ok.

>>> > > BTW2: There is a "role chain" entry in the "Role constructors"  
>>> > > cell. Shouldn't it be getting checked, when I press the "OWL1.1"  
>>> > > button? That's one of the new features of OWL1.1, AFAIK. 
>>> > > Currently,  this checkbox keeps unchecked. When I check it
>>> > > manually, the complexity again changes to "NExpTime-hard".
>> > 
>> > I call out to Evgeny :)
> 
> OWL 1.1 has NO role chain per se. What it has is complex role inclusion axioms, with a
> role chain on the left hand side and a role on the R.H.S. Whereas to have a role chain in
> a logic means to use it everywhere (in number restrictions, in transitivity axioms, in
> role inclusion axioms, etc), which is undecidable. That's why that checkbox is not getting
> checked.

Ok, I see that the "R" checkbox (lower right cell) really gets checked
when pressing "OWL1.1" ("R" in "SROIQ" aka OWL1.1).

But if general role chaining is undecidable, why then is the result for
"OWL1.1+roleChain" just "NExpTime-hard"? Not wrong, of course, but
couldn't one just say "undecidable"?

BTW: I found a typo in note 6, last sentence: "As fo_r_ logics...",
missing "r".


Bijan Parsia wrote on Wed, 7 Mar 2007 00:23

> 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))"""

Ok, "C-co" here is the "other" class, which can also have some 
definition elsewhere:

   Class(C-co complete <expr2>)

The latter two number restriction (re)definitions are obviously 
disjoint. And as long as property "P" really is never used nowhere by 
nobody (maybe some "forbidden" URI "P" can be used for this), than this 
is really equivalent to a disjointness axiom for C and C-co. Co-ol! :-)

Many thanks for this (these thanks, of course, also goes to the original 
authors of this example)!


Cheers,
Michael


[1] OWL1.1 Overview
     http://owl1-1.cs.manchester.ac.uk/overview.html

Received on Wednesday, 7 March 2007 18:54:53 UTC