Galigator / openllet

Openllet is an OWL 2 reasoner in Java, build on top of Pellet.
https://www.w3.org/TR/owl2-primer/
Other
100 stars 26 forks source link

ArrayIndexOutOfBoundsException when using minQualifiedCardinality #57

Open broektjvd opened 3 years ago

broektjvd commented 3 years ago

I ran into a problem with what seems to be a bug with the minQualifiedCardinality axiom. It exists in Pellet as well, but when using HermiT there is no problem. There are workarounds of course but I would like to be able to use this axiom as it was meant to work.

The error it throws is as follows:

java.lang.ArrayIndexOutOfBoundsException: Index 2 out of bounds for length 2
        at openllet.core.tableau.branch.DisjunctionBranch.tryBranch(DisjunctionBranch.java:164) ~[openllet-core-2.6.5.jar:2.6.5]
        at openllet.core.tableau.branch.Branch.tryNext(Branch.java:130) ~[openllet-core-2.6.5.jar:2.6.5]
        at openllet.core.tableau.completion.SROIQStrategy.backtrack(SROIQStrategy.java:112) ~[openllet-core-2.6.5.jar:2.6.5]
        at openllet.core.tableau.completion.SROIQStrategy.complete(SROIQStrategy.java:170) ~[openllet-core-2.6.5.jar:2.6.5]
        at openllet.core.boxes.abox.ABoxImpl.lambda$isConsistent$12(ABoxImpl.java:1417) ~[openllet-core-2.6.5.jar:2.6.5]        at openllet.core.utils.Timers.execute(Timers.java:118) ~[openllet-core-2.6.5.jar:2.6.5]

It goes on for a while but this probably the most relevant part.

I've had the problem with several ontologies but below is the simplest ontology that I could make that triggers the exception:

@prefix : <http://test.org#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix xml: <http://www.w3.org/XML/1998/namespace> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@base <http://test.org> .

<http://test.org> rdf:type owl:Ontology .

:rel rdf:type owl:ObjectProperty .

:class rdf:type owl:Class .
:one rdf:type owl:Class .
:two rdf:type owl:Class .
:three rdf:type owl:Class .
:four rdf:type owl:Class .

:subclass rdf:type owl:Class ;
          owl:equivalentClass [ rdf:type owl:Restriction ;
                                owl:onProperty :rel ;
                                owl:minQualifiedCardinality "2"^^xsd:nonNegativeInteger ;
                                owl:onClass [ rdf:type owl:Class ;
                                              owl:unionOf ( :four
                                                            :three
                                                            :two
                                                            :one
                                                          )
                                            ]
                              ] ;
          rdfs:subClassOf :class .

:first rdf:type owl:NamedIndividual, :one .

:member rdf:type owl:NamedIndividual, :class ;
        :rel :first, :second .

:second rdf:type owl:NamedIndividual, :two .

[ rdf:type owl:AllDifferent ;
  owl:distinctMembers ( :first
                        :member
                        :second
                      )
] .