OWL 2 profiles datatype definition issues

[linkvt]

Hi,

I used the OWL 2 EL, QL and RL profile to validate some smaller ontologies I created. At some point I noticed that the OWL API did - at least to my knowledge - behave incorrectly. I then used the OWL 2 Profiles document to test the three profiles. The following ontologies, which were created with the OWL API 4.0.2, cause validation errors for me which I don't understand.

OWL 2 EL
I get the message "Use of unsupported data range" a few times.
"Use of data range not in profile" for DataOneOf.

OWL 2 QL
Again "Use of unsupported data range". Also "Axiom type not allowed in profile" for the DisjointClasses.
Although I don't get the violation "Axiom type not allowed in profile" when using the OWL Validator with AllDisjointClasses andowl:DisjointWith.
The profiles document says IrreflexiveObjectProperty is allowed, the listing on the bottom of the page doesn't contain it. Because of this I'm not sure what the correct behaviour is.

OWL 2 RL
"Use of unsupported data range" when using the same elements as in the other ontologies.
EquivalentDataProperties, DataIntersectionOf, DisjointDataProperties, DisjointClasses should be allowed, but I receive "Axiom type not allowed in profile".

Also "ReflexiveProperty" should not be allowed (example), but the profile doesn't complain (profiles page: "OWL 2 RL supports all axioms of OWL 2 apart from disjoint unions of classes (DisjointUnion) and reflexive object property axioms (ReflexiveObjectProperty)").

I hope that this might help and already thanks for looking into it. As I'm not very familiar with OWL I hope not all of my findings are wrong.

Edit: I updated the ontologies to use datatypes OWL 2 profiles allow.

[sesuncedu]

The putative EL ontology contains and uses:

:EvenIntegers rdf:type rdfs:Datatype .
:OddIntegers rdf:type rdfs:Datatype .

Which are not part of the explicitly listed set of permissible data types.

(This applies to all three profiles- my MacBook was having a little heat death- only happened to know it applied EL off the top of my head)

[sesuncedu]

Disjoint classes might be over excluded. It was being blocked in the EL checker by mistake until a few versions ago, so I am suspicious

[sesuncedu]

RL profiler does improperly reject DataIntersectionOf, though it should reject the intersection in the example, since the conjuncts are not in RL.

[sesuncedu]

QL improperly rejects DisjointClasses

[linkvt]

Thanks for the info about the illegal datatypes, I totally forgot there is a whitelist.

I updated the ontologies listed above; older revisions are still available in the gist.

[ignazio1977]

DataIntersection in RL fixed

DisjointClasses in QL fixed

[ignazio1977]

Side note: the validator URL points to a tool based on an old version of the OWL API - there's a chance that there are bugs in there, so do not take it as a reference :-) it could be wrong.

[ignazio1977]

QL specs say: reflexive and irreflexive allowed. The fact that they're not listed might be a typo. I believe they should be allowed (unlikely to be two typos in a row in the textual description).

[ignazio1977]

QL irreflexive fixed. RL to be done after lunch because reasons.

[ignazio1977]

This should be fixed in version4 - do you have a chance to check out and build it locally, @linkvt ? Otherwise I'll upload a new snapshot to Sonatype.

[linkvt]

@ignazio1977 I tried to use the locally built jars but without success. Importing the owl api project in IDEA also didn't work for me. Both times I received errors when running the application.
If you could tell me how to make it work, I will try it. If you're more comfortable with creating a new snapshot, it would also be OK.

[ignazio1977]

New snapshot available here: https://oss.sonatype.org/content/repositories/snapshots/net/sourceforge/owlapi/owlapi-distribution/4.1.0-RC4-SNAPSHOT/

[linkvt]

@ignazio1977 Thanks for the fixes and the snapshot. The QL and RL ontologies pass the validation now.

The OWL 2 EL profile still reports a violation:

Use of data range not in profile:

<.../DataOneOfSingleLiteral> [DatatypeDefinition(<.../DataOneOfSingleLiteral> DataOneOf("singleLiteral"^^xsd:string )) in OntologyID(OntologyIRI(<...>) VersionIRI(<null>))]]

I don't understand this because it seems OK when looking at the following rules:

Datatype := IRI

DataOneOf := 'DataOneOf' '(' Literal ')'
DataRange := Datatype | DataIntersectionOf | DataOneOf

DatatypeDefinition := 'DatatypeDefinition' '(' axiomAnnotations Datatype DataRange ')'

Is this because of the restricted set of datatypes sesuncedu pointed out? If it is, how can a DatatypeDefinition exist in the OWL 2 EL profile?

[ignazio1977]

Where the list of supported datatypes is mentioned, there's also this:

The set of supported datatypes has been designed such that the intersection of the value spaces of any set of these datatypes is either empty or infinite, which is necessary to obtain the desired computational properties [EL++].

To me this implies that any other datatype defined must match this as well - I'd think that, given this, it is not possible to define new datatypes that intersect these value spaces at all. I'm not sure why DatatypeDefinition is allowed in the grammar, as I cannot think of a case in which it would be used that did not fall outside EL.

However, I do not consider myself an expert on the topic, so I cannot give you a definitive answer.

[linkvt]

Thanks for your perspective on this, I will look into it and add it here if it affects the OWL API validation.
But for now this issue is resolved, so thank you both for the support!

[ignazio1977]

marking the fix to be ported to version 5

[sesuncedu]

I am convinced that the error in the Profile specification with respect to EL, and possible others, is that names defined by datatype definitions are not added to the set of admissible data ranges.

From the Abstract & Fun Syntax Spec

9.4 Datatype Definitions

A datatype definition DatatypeDefinition( DT DR ) defines a new datatype DT as being semantically equivalent to the data range DR[...]. This axiom allows one to use the defined datatype DT as a synonym for DR — that is, in any expression in the ontology containing such an axiom, DT can be replaced with DR without affecting the meaning of the ontology.

And

11.2 The Restrictions on the Axiom Closure
[...]
A strict partial order (i.e., an irreflexive and transitive relation) < on the set of all datatypes in Ax exists such that, for each axiom of the form DatatypeDefinition( DT DR ) and each datatype DT1 occurring in DR, we have DT1 < DT. [... ]
[This] condition ensures that datatype definitions are acyclic

Thus we can finitely expand the datatype definition, and the expansion can only contain EL legal constructs.

Also, if the DT argument is not added to the set of admissible datatypes, then DatatypeDefinition could at most be syntactically used to attempt to redefine a datatype listed in the whitelist. This is blocked by section 4, which specifies the lexical and value spaces for each of these types. Since defined types have empty lexical spaces, this eliminates every DT apart from owl:real; however, owl:real is given a specified value space, which can only be expressed as owl:real, violating the strict partial order. Further, owl:real has defined facets, but the result would not (this isn't as relevant for EL).

There are some unnecessary restrictions in the OWL 2 Profiles, but this seems like scrivener's error.

[sesuncedu]

Time for a sad message to public-owl-comments.

[sesuncedu]

This looks like a problematic commit.

5962497

[sesuncedu]

Also, DisjointClasses in RL and QL aren't checking to see if the elements are subclasssexpressions.
Will fix once I can run a compiler.

This code was right in owlapitools.
All of the errors apart from the disjointclasses ones seem to be in owlapitools.

[ignazio1977]

Aha. We had profile verification implemented but not run as part of the build. I assumed the tests were correct. Silly me.

[ignazio1977]

Fixed QL and RL as they should have been.

[ignazio1977]

The bugs have been fixed. The remaining problem is an issue with the specs - marked as such.