Disjoint classes inference resolution time

[areleu]

This might be a very basic question but I have not found a definitive reference for this. The inference of Disjoint classes is very slow. And I understand from the cues in Protegé that itself the operation is very slow.

If I try to perform it with an ontology with more than 40 disjoint class axioms it seems to never end the calculation (I have been using Protegé and ROBOT for this, not the reasoner nor the OWLAPI directly). Are more than 40 disjointness axioms too many for the reasoner or is there a possibility of some other underlying problem with the ontology?

I hope someone can enlighten me on this because I am at loss. (if this is for any reason explainable with theory I am happy to know about some references I can read)

Here is the related issue OpenEnergyPlatform/ontology#1465 (comment)

[ignazio1977]

I'm guessing that "inference of disjoint classes" refers to the materialization of axioms through inferred axiom generators? If so, a while ago there were bugs raised - in short, the inferred axiom generator was vastly inefficient. Those issues were sorted quite a long time ago, but whether they've been sorted for the code you're using would depend a lot on OWLAPI amd HermiT versions you're working with (if going through ROBOT, then I assume the ROBOT version would be the main determinant).

Can you add any information you have about versions here? (Or on the owlcs/hermit-reasoner fork of this project)

[areleu]

I'm guessing that "inference of disjoint classes" refers to the materialization of axioms through inferred axiom generators? If so, a while ago there were bugs raised - in short, the inferred axiom generator was vastly inefficient. Those issues were sorted quite a long time ago, but whether they've been sorted for the code you're using would depend a lot on OWLAPI amd HermiT versions you're working with (if going through ROBOT, then I assume the ROBOT version would be the main determinant).

Can you add any information you have about versions here? (Or on the owlcs/hermit-reasoner fork of this project)

Sure. I have been using the latest ROBOT version 1.9.3 which in place uses HermiT 1.3.8.413. As for Protegé I have been using 5.6.1 which uses 1.4.3.456. When trying to infer the Disjoint classes of all the classes in the ontology the former just gets stuck and the latter seems to be properly inferring the classes but becomes very slow, which tells me that it is probably just still calculating.

[ykazakov]

@areleu How many classes are in your ontology (including all imports)? I think computing disjoint classes is not much different than testing all pairs of classes for disjointness. This results in a quadratic number of tests in the number of classes. This is probably a main reason why this type of inference is disabled in Protege by default. In my understanding, the number of disjoint class axioms should not be that important -- and this could be easily checked by commenting out all such axioms.

[areleu]

@areleu How many classes are in your ontology (including all imports)? I think computing disjoint classes is not much different than testing all pairs of classes for disjointness. This results in a quadratic number of tests in the number of classes. This is probably a main reason why this type of inference is disabled in Protege by default. In my understanding, the number of disjoint class axioms should not be that important -- and this could be easily checked by commenting out all such axioms.

We are talking of a little more than 1400 classes. And you are right, I deactivated most of the Disjoint class axioms and still have the same outcome.

I removed all the disjoint class axioms that are in the ontology and kept the BFO 2.0 disjoint class axioms. The outcome was the same as I mentioned before. But if I do the reasoning on the BFO 2.0 alone it resolves in a very short time. So I think it definetively has to do with the number of classes

[ykazakov]

1400 * 1400 = 1960000, so there are about 2M disjointness tests. According to this information BFO 2.0 has just 35 classes, so 35 * 35 = 1225 disjointness tests. A huge difference! Furthermore, since BFO is smaller, each disjointness test is faster, adding another factor to the difference.

[areleu]

Thanks everyone. It is clear that this is just a problem of magnitude. If you think that there is nothing in the reasoner implementation that can improve this situation then feel free to close this issue.