Re: Problematic interesectionOf construct for determining OWL Lite dialect

On 2 Nov 2011, at 12:11, Ondrej Zamazal wrote:

> Hello,
> I was inspecting what constructs are admissible in OWL Lite

OWL Lite is totally irrelevant now. I strongly strongly recommend ignoring it entirely.

(It's design was broken from the start and no tools that I know of target it in any interesting way. Old species validators are not being updated.)

If you need to focus on a subset of OWL, then the profiles (OWL EL, QL, and RL) are the way to go.

> and I have encountered on strange things regarding OWL species returned by OWL Validator [1] and by Protégé-OWL version 3.4.7.

Oy. I really can't face going into the Semantics and Abstract syntax document, so everything I say may be dodgy. Oh, damn it, I can't consult the reference. Anyway:
	http://www.w3.org/TR/owl-semantics/syntax.html#2.3.1

> My main concern is about "intersectionOf" construct. Looking at [2] "OWL Lite allows intersections of named classes and restrictions". This means that
> 
> C2 subClassOf C1 and (p1 some C2)

That looks to be legal OWL Lite.

> should be still valid axiom from OWL Lite perspective. However, if you try "determine OWL sublanguage" in Protégé then it returns OWL DL for this case, which is wrong. The wrong result is also returned by OWL Validator [2]. But if there is "equivalentTo" instead of "subClassOf" then OWL Validator returns "OWL Lite" correctly while Protégé still returns "OWL DL".

It depends on the surface syntax (BONKERS)! If you serialize it according to the frame based syntax:

	Class(' classID ['Deprecated'] modality { annotation } { super } ')'

Then with modality "complete" you could express it. But if you use and EquivalentClasses axiom:
	axiom ::= 'EquivalentClasses(' classID classID { classID } ')'

Then it wouldn't be OWL Lite! since you should have only Class IDs.

*Run screaming into the night.*

It's totally not worth tracking this down in code. I'll see if I can get someone to put a big warning sign on the validator.

> Then, I realized that if you directly decompose "intersectionOf" construct into an appropriate number of subclasses/equivalences than it is always correct in the case of OWL Validator. In the "minimalistic" case the following is incorrectly classified as axiom from OWL DL using OWL Validator and Protege:
> 
> A subclassof (B and C)
> 
> If there are two following axioms (which is equivalent representation), it is then correctly classified as OWL Lite by both OWL Validator and Protege, i.e.:
> 
> A subclassof B
> A subclassof C
> 
> In the case of Protege there are some further unclear cases even if "intersectionOf" is decomposed e.g.
> 
> A subclassof (p1 some C2)
> A subclassof C
> 
> is correctly classified as OWL Lite. However,
> 
> A equivalentTo (p1 some C2)
> A equivalentTo C
> 
> is wrongly classified as OWL DL by Protege.

I'm betting that the serializaiton is tripping things up. Best guess.

> I am aware that now we are in the age of OWL 2 so maybe these notes are already obsolete, however I wanted to share with you about those unclear OWL dialect results. But it might also be the case that  I missed some point?

The only point I can see is if they parse them to different structure there are diverse correct results :(

But this isn't worth your time, really. We should clearly mark all such validators as deprecated. There are no good expressivity checkers, IMHO, at the moment. In particular, there are none (except some code in CB which may be in ELK too) that look beyond the surface spelling and take polarity into account. Getting that right would be superduper useful.

Cheers,
Bijan.

Received on Friday, 4 November 2011 08:44:38 UTC