Finalise definition of base release

[matentzn]

This tiny PR may be one of the most consequential in the history of ODK, so let's get it 100% right.

What we are doing here is enshrining in stone 2 years worth of debates on how to define base modules for proper ontology dependency management. The debates happened, for better or worse, behind closed doors - it took just four of us (@cmungall, @balhoff, @dosumis and me) roughly 2 years to grudgingly agree on a middle ground.

The full specification can be found here: OBOAcademy/obook#387

What does this PR do?

1. The definition of the "base" file is now changed. Previously, the base was simply "all the axioms the editors have provided", without any concerns for reasoning or redundancy. The old base reflects the structure of the editors file with no instantiation of axioms inferred by a reasoner. The new base reflects the structure of the ontology release file, including (a non-redundant set of) whatever instantiated reasoner-inferred axioms the authors of the ontology have chose to include in the release. This may include inferred subClassOf axioms between named classes and materialised existential restrictions. You can check out the exact sequence of ROBOT commands in this pull request to get the picture.
2. The old base release (all the axioms managed by the ontology editors, as they are, with no subclass-graph reduction and no reasoning) is now called "baselite" release
3. The "base merging" approach in ODK now has an option, switched on by default, to remove equivalent class axioms prior to extracting a module. This way externally provided classifications are protected again axiom injection ("trust the source" principle)

[dosumis]

"base" axioms are axioms that use at least one "base" entity. This is the current definition in ROBOT ontodev/robot#570, and it is not ideal; consider the case EXTERNAL:A subClassOf EXTERNAL:R some BASE:B - we really don't want this in our base release.

From discussion on call, I believe base-plus moved to using axiom tagging. If so, could this be made clear? If the interests of progress, we could decide not to make this a blocker, but fixing is very urgent. This potentially pulls massive numbers of axioms from imports into base, including axiom injections (axioms that change the definition of base entities). This goes against the whole rationale of having a base.

---

EDIT @matentzn moved a @dosumis comment here.

---

Now, it is defined as "the ontology with all non-redundant base axioms".

We need clearer doc than this. I don't think this communicates the nature of the change - the old base reflects the structure of the editors file with no instantiation of axioms inferred by a reasoner. The new base reflects the structure of the ontology release file, including (a non-redundant set of) whatever instantiated reasoner-inferred axioms the authors of the ontology have chose to include in the release. This may include inferred subClassOf axioms between named classes and materialised existential restrictions.

[matentzn]

From discussion on call, I believe base-plus moved to using axiom tagging. If so, could this be made clear? If the interests of progress, we could decide not to make this a blocker, but fixing is very urgent. This potentially pulls massive numbers of axioms from imports into base, including axiom injections (axioms that change the definition of base entities). This goes against the whole rationale of having a base.

I forgot to update the text in here, we had already made some progress on this during our last call:

"base" axioms are axioms that use at least one "base" entity. This is the current definition in ROBOT pr. We have added issue #819 - but we have been using this process for a while now without any issues. During our last Monarch Ontology Tools call, we have reviewed the functionality briefly and determined that it "looks correct".

I have documented the next step for dealing with this (and a vote) in this ticket here: #819

"the ontology with all non-redundant base axioms": We need clearer doc than this. I don't think this communicates the nature of the change - the old base reflects the structure of the editors file with no instantiation of axioms inferred by a reasoner. The new base reflects the structure of the ontology release file, including (a non-redundant set of) whatever instantiated reasoner-inferred axioms the authors of the ontology have chose to include in the release. This may include inferred subClassOf axioms between named classes and materialised existential restrictions.

I have updated the text above in my comment to get that across. I also added this ticket: #825

[dosumis]

I'm now satisfied with the description of the new behaviour and of (roughly) how this is achieved. It would be good to get a more detailed review of the series of robot commands from others.