Check of DL profile fails for axioms with dublicate arguments

[tobiaswjohn]

I encountered the problem that a valid OWL DL ontology can be classified as not belonging to OWL DL if the same argument is used twice in an EquivalentClasses-axiom. Here is a minimal ontology:

Prefix(:=<http://www.example.org/reasonerTester#>)

Ontology(
  Declaration(Class(:A))
  EquivalentClasses(:A :A)
)

Using the class OWL2DLProfile(), I wrongly get a violation report for the OWL DL profile. According to the definition of EquivalentClasses in the OWL DL standard, the axiom is equivalent to two SubClassOf(:A :A) axioms. The latter representation gets correctly classified by OWL2DLProfile() as contained in OWL DL.

I think, the issue is triggered by how the axiom is parsed in OWLFUctionalSyntaxParser where the arguments are parsed as a set in this function. In short: the way the axiom is parsed and how the profile is checked are conflicting.

A similar issue also occurs for other types of axioms in OWL DL. I found the following one:

• SameIndividual
• EquivalentDataProperties
• EquivalentObjectProperties
• ObjectIntersectionOf
• DataIntersectionOf

For reproduction, here is a minimal program that demonstrates the behavior:

OWLOntologyDocumentSource source = new FileDocumentSource(ontFile, new FunctionalSyntaxDocumentFormat());
OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
ont = manager.loadOntologyFromOntologyDocument(source);

OWLProfileReport profileReport = new OWL2DLProfile().checkOntology(ont);
List<OWLProfileViolation> violations = profileReport.getViolations();

[ignazio1977]

It's not incorrectly detected :-)

This issue is famous. About a decade ago it was discussed at length.

While the intended meaning is the same as two identical subclass axioms, or just one in fact, the syntax in the specs gave rise to misunderstandings.

The agreement reached, which included some of the spec authors, was that the arguments to those axioms are expressed as lists but are actually sets. Passing the same element twice means one copy is discarded. And the cardinality constraint means that a valid axiom needs two or more distinct arguments, so one with a single argument fails the constraints.

[tobiaswjohn]

I see. I think this agreed interpretation of the standard is not obvious for everyone.
Maybe one can add a note in the string representation of the violation report that the arguments are interpreted as a set? This would provide some clarification, why this is not allowed and why the arguments where unified.