Incorrect result depending on concept names

[tobiaswjohn]

I am using Openllet to decide the consistency of an ontology and compute inferred axioms. I encountered unexpected behavior, where changing the name of a class, a role or an individual leads to a differenr result. I.e., Openllt computes the wrong result in some cases. As far as I can see, the behavior of the reasoner should not change after renaming in all of the examples. I will present three examples, where this behavior occurs:

Example 1

• Ontology in functional syntax:

Prefix(:=<http://www.example.org/reasonerTester#>)
Prefix(rdfs:=<http://www.w3.org/2000/01/rdf-schema#>)

Ontology (
	Declaration(NamedIndividual(:a))
	Declaration(NamedIndividual(:c))
	Declaration(ObjectProperty(:rsim))
	Declaration(ObjectProperty(:snonsim))
	Declaration(DataProperty(:dp))
	Declaration(DataProperty(:dr))
	
	EquivalentClasses(
	    ObjectHasSelf(:rsim) 
	    ObjectOneOf(:c)		# renaming :c to :a makes a difference
	    ObjectSomeValuesFrom(:snonsim DataSomeValuesFrom(:dp rdfs:Literal)) 
	    DataHasValue(:dr "s") 
	)
	
	DataPropertyDomain( 
	    :dp 
	    DataHasValue(:dr "s")
	)
)

• The problem:
  Openllet infers that the ontology is inconsistent. I cross-checked the consistency with HermiT, which classified the ontology as consistent.
• The result of the consistency check seems to depend on the name of the individual in the EquivalentClass axiom. The ontology is correctly classified as consistent, if one uses the individual :a instead of :c.

Example 2

• Ontology in functional syntax:

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

Ontology (
	Declaration(Class(:A))
	Declaration(Class(:D))
	Declaration(NamedIndividual(:a))
	Declaration(NamedIndividual(:d))
	Declaration(ObjectProperty(:s))
	Declaration(ObjectProperty(:r))
		
	EquivalentClasses(  
	    ObjectOneOf(:d) # renaming :d to :a prevents bug
	    ObjectSomeValuesFrom(:s :D)     # renaming :D to :A prevents the bug 
	    ObjectHasSelf(:r) 
	)
)

• The problem:
  Openllet infers the axiom SymmetricObjectProperty(:s), which is not entailed by the ontology.
• The result of the inference seems to depend on the name of the individual and class used in the EquivalentClass axiom. E.g., the incorrectly inferred axiom disappears if one uses the individual :a instead of :d or the class :A instead of :D.

Example3

• Ontology in functional syntax:

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

Ontology (
	Declaration(Class(:C))
	Declaration(NamedIndividual(:a))
	Declaration(NamedIndividual(:d))
	Declaration(ObjectProperty(:qsim))
	
	EquivalentClasses(  
	    ObjectHasSelf(:qsim) 
	    ObjectOneOf(:d) 
	    :C 
    )
)

• The problem:
  Openllet infers the axiom ClassAssertion(:C :a), which is not entailed by the ontology.
• The result of the inference seems to depend on the name of the individual, class and relation used in the EquivalentClass axiom. E.g., incorrect inference disappears if one uses the individual :a instead of :d or the relation name :r instead of :qsim.

Code

• For reproduction, here is the call from my program using OWL API:

OWLOntologyDocumentSource source = new FileDocumentSource(ontFile, new FunctionalSyntaxDocumentFormat());
OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
ont = manager.loadOntologyFromOntologyDocument(source);
OWLReasoner openllet = OpenlletReasonerFactory.getInstance().createReasoner(ont);

openllet.isConsistent()

List<InferredAxiomGenerator<? extends OWLAxiom>> gens = new ArrayList<>();
gens.add( new InferredObjectPropertyCharacteristicAxiomGenerator());
gens.add( new InferredClassAssertionAxiomGenerator());

InferredOntologyGenerator iog = new InferredOntologyGenerator(openllet, gens);
OWLOntology infOnt = manager.createOntology();
iog.fillOntology(ont.getOWLOntologyManager().getOWLDataFactory(), infOnt);