Konclude not seeing pigeonhole principle

[mpomarlan]

Hello,

I encountered a situation in which HermiT arrives at a (correct) conclusion which Konclude misses. The OWL file is as follows:

Prefix(:=<http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/>)
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#>)

Ontology(<http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole>

############################
#   Object Properties
############################

# Object Property: :sitsAt (:sitsAt)
SubObjectPropertyOf(:sitsAt owl:topObjectProperty)

############################
#   Classes
############################

# Class: :CrowdedHole (:CrowdedHole)
EquivalentClasses(:CrowdedHole ObjectIntersectionOf(:Hole ObjectMinCardinality(2 ObjectInverseOf(:sitsAt) :Pigeon)))
SubClassOf(:CrowdedHole :Hole)

# Class: :CrowdedScene (:CrowdedScene)
EquivalentClasses(:CrowdedScene ObjectIntersectionOf(:Scene ObjectSomeValuesFrom(ObjectInverseOf(:inScene) :CrowdedHole)))
SubClassOf(:CrowdedScene :Scene)

# Class: :Hole (:Hole)
EquivalentClasses(:Hole ObjectOneOf(:h1 :h2))
SubClassOf(:Hole ObjectSomeValuesFrom(:inScene :Scene))

# Class: :Pigeon (:Pigeon)
EquivalentClasses(:Pigeon ObjectOneOf(:p1 :p2 :p3))
SubClassOf(:Pigeon ObjectExactCardinality(1 :sitsAt :Hole))

# Class: :Scene (:Scene)
EquivalentClasses(:Scene ObjectOneOf(:s))

############################
#   Named Individuals
############################

SubClassOf(ObjectIntersectionOf(:Hole :Pigeon) owl:Nothing)
SubClassOf(ObjectIntersectionOf(:Hole :Scene) owl:Nothing)
SubClassOf(ObjectIntersectionOf(:Pigeon :Scene) owl:Nothing)
DifferentIndividuals(:p1 :p2 :p3)
)

With the above file called pigeonhole.owl, I run the command

Konclude classification -i pigeonhole.owl -o output.owl

The contents of output.owl are as follows:

<?xml version="1.0" encoding="UTF-8"?>
<Ontology xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns="http://www.w3.org/2002/07/owl#" xmlns:xml="http://www.w3.org/XML/1998/namespace" xmlns:xsd="http://www.w3.org/2001/XMLSchema#">
    <Prefix name="" IRI="http://www.w3.org/2002/07/owl#"/>
    <Prefix name="owl" IRI="http://www.w3.org/2002/07/owl#"/>
    <Prefix name="rdf" IRI="http://www.w3.org/1999/02/22-rdf-syntax-ns#"/>
    <Prefix name="xml" IRI="http://www.w3.org/XML/1998/namespace"/>
    <Prefix name="xsd" IRI="http://www.w3.org/2001/XMLSchema#"/>
    <Prefix name="rdfs" IRI="http://www.w3.org/2000/01/rdf-schema#"/>
    <Declaration>
        <Class IRI="http://www.w3.org/2002/07/owl#Nothing"/>
    </Declaration>
    <Declaration>
        <Class IRI="http://www.w3.org/2002/07/owl#Thing"/>
    </Declaration>
    <Declaration>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Scene"/>
    </Declaration>
    <SubClassOf>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Scene"/>
        <Class IRI="http://www.w3.org/2002/07/owl#Thing"/>
    </SubClassOf>
    <Declaration>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Hole"/>
    </Declaration>
    <SubClassOf>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Hole"/>
        <Class IRI="http://www.w3.org/2002/07/owl#Thing"/>
    </SubClassOf>
    <Declaration>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Pigeon"/>
    </Declaration>
    <SubClassOf>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Pigeon"/>
        <Class IRI="http://www.w3.org/2002/07/owl#Thing"/>
    </SubClassOf>
    <Declaration>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/CrowdedScene"/>
    </Declaration>
    <SubClassOf>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/CrowdedScene"/>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Scene"/>
    </SubClassOf>
    <Declaration>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/CrowdedHole"/>
    </Declaration>
    <SubClassOf>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/CrowdedHole"/>
        <Class IRI="http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/Hole"/>
    </SubClassOf>
</Ontology>

The Konclude I used is version 0.7.0 (from the activity log: Reasoner for the SROIQV(D) Description Logic, 64-bit, Version v0.7.0-1135 - 91b3e331 (Mar 16 2021)).

The missing conclusion (which HermiT finds) is that CrowdedScene and Scene are equivalent.

I tried realization as well, and the individual s is discovered to be a Scene and a Thing, but it is not discovered to be a CrowdedScene.

[blokhin]

Looks interesting... @irygaev should we also check this with our FaCT++ python bindings / rdflib?

[andreas-steigmiller]

Thanks for the report. It seems that one optimization technique (completion graph caching) does not work completely correctly in this rather special case. If it is deactivated, then Konclude seems to calculate the correct result, e.g., if Konclude is executed with the following command:

Konclude classification -i pigeonhole.owl -o output.owl +=Konclude.Calculation.Optimization.CompletionGraphCaching=FALSE

Nevertheless, it certainly sounds like it can be fixed.

[mpomarlan]

Can confirm, the workaround gets the expected result, and performance on another ontology I actually care about is apparently not degraded.

(Performance on a larger pigeonhole example is, just as in HermiT's case, very bad timewise -- but this is by design since the pigeonhole principle seems to be something many/most reasoners don't find easy to prove.)

I would keep the issue open however. Cannot promise anything but I see there is a paper out explaining how the completion graph cache is supposed to work, and maybe I can throw my eyes on that too and see where the pigeons confuse it.

[mpomarlan]

I have started investigating where this issue might come from. I haven't found a new idea yet but playing with the pigeonhole principle revealed another bug.

Below is a simpler version of the pigeonhole problem -- only 1 hole and 2 pigeons. As far as I can tell, no non-deterministic choices are needed during inference. Konclude does find that Hole and CrowdedHole are equivalent, which is expected.

However (depending on the presence of an axiom that is redundant), Konclude will miss the observation that a Scene is equivalent to CrowdedScene. This happens regardless of whether completion graph caching is enabled or not.

Prefix(:=<http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole/>)
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#>)

Ontology(<http://www.semanticweb.org/blandcorporatio/ontologies/pigeonhole>

# Class: :CrowdedHole (:CrowdedHole)
EquivalentClasses(:CrowdedHole ObjectIntersectionOf(:Hole ObjectMinCardinality(2 ObjectInverseOf(:sitsAt) :Pigeon)))

# This one axiom causes a conclusion to be missed
SubClassOf(:CrowdedHole :Hole)

# Class: :CrowdedScene (:CrowdedScene)
EquivalentClasses(:CrowdedScene ObjectIntersectionOf(:Scene ObjectSomeValuesFrom(ObjectInverseOf(:inScene) :CrowdedHole)))

# Class: :Hole (:Hole)
EquivalentClasses(:Hole ObjectOneOf(:h1))
SubClassOf(:Hole ObjectSomeValuesFrom(:inScene :Scene))

# Class: :Pigeon (:Pigeon)
EquivalentClasses(:Pigeon ObjectOneOf(:p1 :p2))
SubClassOf(:Pigeon ObjectExactCardinality(1 :sitsAt :Hole))

# Class: :Scene (:Scene)
EquivalentClasses(:Scene ObjectOneOf(:s))

DifferentIndividuals(:p1 :p2)
)

Removing the subclassof(crowdedhole hole) axiom will produce the expected output, that Scene and CrowdedScene are equivalent, again regardless of whether completion graph caching is used or not.

[andreas-steigmiller]

Many thanks! I can confirm that the wrong result is produced if the SubClassOf(:CrowdedHole :Hole) is present. It seems to be a bug in the tableau algorithm (CCalculationTableauCompletionTaskHandleAlgorithm) regarding the new dynamic expansion to other relevant nodes from the backend cache in certain situations. In fact,

if (!mBackendCacheHandler || !nondeterministic && !mBackendCacheHandler->hasConceptInAssociatedFullConceptSetLabel(assocData, assocData->getLabelCacheEntry(CBackendRepresentativeMemoryLabelCacheItem::FULL_CONCEPT_SET_LABEL), concept, conNegation, !nondeterministic, calcAlgContext)) {
    expansionBlockingCritical = true;
}

should be something like the following (removed !nondeterministic):

if (!mBackendCacheHandler || !mBackendCacheHandler->hasConceptInAssociatedFullConceptSetLabel(assocData, assocData->getLabelCacheEntry(CBackendRepresentativeMemoryLabelCacheItem::FULL_CONCEPT_SET_LABEL), concept, conNegation, !nondeterministic, calcAlgContext)) {
    expansionBlockingCritical = true;
}

Unfortunately, the testing and evaluation framework is not set up at the moment, so I'm currently not completely sure about the (performance) impact of the changes, but I added it to master (cf. https://github.com/konclude/Konclude/commit/d2f12a9168419fa30c5735ea5bfb51d79967c626). The commit also fixes the completion graph caching issues that you found with the first example. In essence, there were some changes that merge nominal nodes into the constructed node (for determining subsumed classes more easily), but in some cases the completion graph caching check was then not enforced (so it was not correctly checked whether some other nodes need some recomputation).

The build may be broken at the moment (due to dependency changes), so I'm not completely sure when there will be a new version released (I will try to fix it, but I'm not sure how long it will take).

[mpomarlan]

Many thanks!

[mpomarlan]

I have tested the current master version with the pigeonhole examples, here are the outcomes.

pigeonhole2: works, with and without completion graph caching. pigeonhole3 and so on: work without completion graph caching. The bug persists if completion graph caching is enabled however.

[andreas-steigmiller]

Hmm, right, I can confirm that it is still not working correctly for the first example. I will look into that.