RE: Question on DL negation

Hi Michael, Bijan, and Uli,

I looked through the mails and either made some amendments to the DL Navigator, or just
have some comments to say. I'll try to be concise, and minimize over-quoting. :)

Michael Schneider wrote:
> "ComplexityClass-hard" is meant to include undecidability.
> Would you mind to add a note on this in the list of notes?

Done (Note 7 on the web page). It was strange to have the Complexity Navigator without a
reference to any Complexity Theory books (and now there is one -- to Papadimitriou's
book).

Michael Schneider wrote:
> 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"?

In fact, it does show "undecidable" IF the selector "Allow/disallow complex roles in
num.restr." is switched to "Allow" position (by default, it's "Disallow"). Probably, it's
sometimes better to have "Allow" by default?... BUT for logics such as ALCF_trans,
ALCIQ_reg (and other with _trans or _reg subscript) it is traditionally assumed that role
chain, union, star, are DISallowed in number restrictions... (see Note 5 on the web page).

Michael Schneider wrote:
> Perhaps a little more information
> should be added, to distinguish:
> * NExpTime-hard, possibly undecidable
> * NExpTime-hard, proofed as decidable

Good idea. I would only add that "NExpTime-hard" per se means "NExpTime-hard, possibly
undecidable". So, only lower bounds for decidable logics should be added.

I have done this for RIQ, sROIQ and logics in between, and will look what can be done for
other logics later.

Ideally, the Navigator should compute TWO complexities (lower and upper) for a given
logic. If they coincide, it should infer "SomeClass-complete", otherwise it should show
both. Indeed, we have always for free the upper bound "undecidable" and the lower bound
"PSpace-hard" (since my Navigator starts with ALC).

Example:
OWL 1.1 = between NExpTime-hard and decidable
OWL 1.1 + RoleChain = between NExpTime-hard and undecidable

However, strictly speaking, complexity classes are NOT linearly ordered, so TWO
complexities may be even not enough.

A final comment: the DL Navigator, while being (hopefully) correct (i.e., showing correct
results), is incomplete even w.r.t. itself (!), i.e. it sometimes could show a stronger
result than it shows. This mainly concerns to "incomplete cases" (when it says
SomeClass-hard, or "decidable"). The most elegant way to "complete" the Navigator would be
to build an Ontology of DLs, so that one could INFER the lower and upper bound from the
known results.

Anyway, thank you all for the feedback.

Cheers, Evgeny

Received on Thursday, 8 March 2007 09:18:41 UTC