It seems that if the axiom is a tautology (is entailed from the empty set of axioms), incorrect explanations are produced.
To reproduce:
open any ontology, e.g., Pizza
go to DL Query tab and enter some conjunction, e.g., American and Pizza
compute the superclasses of the query
press explain (?) next to the conjunct appearing in the query, e.g., "Pizza"
Expected result:
only the empty explanation should be shown
Actual result:
the computation does not seem to terminate; if interrupted it shows many explanations with one axiom from the ontology but also with some axioms like \<Entailmentxxxxx> SubClassOf ...
It seems that if the axiom is a tautology (is entailed from the empty set of axioms), incorrect explanations are produced.
To reproduce:
Expected result: only the empty explanation should be shown
Actual result: the computation does not seem to terminate; if interrupted it shows many explanations with one axiom from the ontology but also with some axioms like \<Entailmentxxxxx> SubClassOf ...