ENVO uses some axioms that are used by Elk 0.4.3, but ignored in Elk 0.5.0

[cmungall]

Noticed by @turbomam

With Elk 0.4.3, atmospheric boundary layer is inferred to be both a atmospheric layer and a boundary layer

Here is the explanation:

The explanation is IMO quite complicated, and we can see it makes use of some disjunctions (OR)

When we switch to Elk 0.5.0 this entailment disappears

Note that our entire stack has moved to 0.5.0, including ROBOT, so getting this back will be difficult

This bug was noticed in a different context by @balhoff

Reported here:
liveontologies/elk-reasoner#61 (comment)

the TL;DR is even though disjunctions were always formally outside the EL++ profile, Elk gave us limited disjunction reasoning "for free", in limited cases for example, structural matching of identical disjunctive expressions. IMO it was always a mistake to depend on this

Path forward

We have two options

1. Revert our stack to using an older ODK, older ROBOT. cc @matentzn
2. Simplify our axioms to never use disjunctions in equivalence axioms, always name disjunctions, and follow simple DPs
3. Do a one time reason with 0.4.3, assert entailed axioms

It should be no surprise that I am massively in favor of 2

[balhoff]

Just want to note that "negative" (subclass side) occurrences of unions are officially supported: https://github.com/liveontologies/elk-reasoner/wiki/OwlFeatures

But I think this explanation is using a positive occurrence on line 3.

[balhoff]

Another option is switching to Whelk; it should infer this.

[matentzn]

Just to make sure we have touched all bases:

1. How much time would it take to run whelk vs elk vs konclude
2. in FBcv, we have the same, and run a small "inferred axiom" component with Konclude (see here)

I would not recommend generally swapping Elk for Whelk to maintain technological homogeneity across all ontologies, but we can do solution (3) as a dynamic component ala FBcv and have it run every two weeks as a workflow.