Search code examples
owlsemantic-webprotege

Protege multiple equivalentTo axioms vs union of axioms

I am trying to understand the difference between using multiple equivalentTo axioms and using a union (i.e., disjunction) of those axioms. I have set up a toy ontology with this structure: Class_A - Class_A.1 Class_B Class_C Class_D - Class_D.1 with an object property named has_part.

Class_A.1 is defined using the equivalence axiom: EquivalentTo (Class_A and (has_part some Class_B)) or (Class_A and (has_part some Class_C))

Class_D1 is defined using two equivalence axioms: EquivalentTo Class_D and (has_part some Class_B) EquivalentTo Class_D and (has_part some Class_C)

Using HermiT 1.3.8.413, I execute the DL Query has_part some Class_B. This returns subclass Class_D.1, which makes sense.

However, I do not understand why Class_A.1 was not returned. I thought since the equivalence axioms for Class_A.1 was a disjunction, it was be subsumed by the has_part some Class_B disjunct.

Solution

  • Let me try a simpler example. We don't necessarily need to bring in object properties to illustrate the concept. We can replace 'has_part some X' with an arbitrarily named class with no change to entailments, since we're not saying anything about X. Also for the purposes of your example, we can leave out the 'A' in list of intersection elements.

    Instead of your A.1, let's try:

    Prokaryote EquivalentTo Bacteria OR Archaea

    Choosing a biological example as I know you're familiar, but for others, Bacteria, Archaea and Eukaryota are the 3 domains of life. The term "prokaryote" refers to an artificial but sometimes useful grouping of bacteria and archaea.

    OK, so now we try the DL query "Bacteria". This doesn't return prokaryotes as a subclass, as we know that actually prokaryotes are a superclass of bacteria.

    Hopefully mapping to this concrete example helps with the underlying intuition. I personally find that UnionOf can be strangely counter-intuitive with abstract examples, but when replaced with concrete examples it's more obvious.

    For a more formal elucidation, I think it suffices to echo ASKW's comments, that equivalence entails mutual subClassOf, but there is no entailment that A subClassOf B or C entails A subClassOf B. Hope this helps.