For discussion, cc @dosumis

Motivation

For various reasons, the release version of an ontology can end up with redundant axioms; e.g.

1. A SubClassOf B
2. B SubClassOf C
3. A SubClassOf C

Here 3 is redundant. Generally this should be pruned from the public release. There may be situations where this is not desired: for example, 3 may be adorned with a useful axiom annotation

How it is used

As part of a release process, after reasoning and after #7

Note on GO-centric corner case: should never be applied to editors ontology as it may cause "ontology autophagy" when used as part of a cached link approach.

Extensions

The notion of redundancy can be extended to the existential graph too, but this is more subtle, and my be best considered out of scope for this op, and a new op developed. The name perform-transitive-reduction or similar should be reserved for this task and @fbastian's code adopted.

Spec

For simplicity we will only consider the graph formed by SubClassOf axioms between named classes. Equivalence axioms are ignored for the purposes of determining redundancy. Thus in the following 1 will be retained

1. A SubClassOf B
2. A EquivalentTo B and R some Z

The user should perform #7 relax step first to ensure a complete SubClassOf axiom graph is present. Motivation: if we use reasoning to determine redundancy it complicates structural and logical requirements (TBD).

If the ontology contains an axiom A SubClassOf Z, and there exist a chain of two or more axioms A SubClassOf B, B SubClassOf ... ... ... SubClassOf Z, then A SubClassOf Z is considered redundant.

Alternate reasoner based way of finding redundancy that does not require pre-reasoning: If the ontology contains an asserted axiom A SubClassOf Z and two inferences, A SubClassOf B, 'B SubClassOf Z` (as determined by the owlapi reasoner api, i.e. proper SubClassOf), then A-Z is redundant.

All redundant axioms are found, and then removed

TODO: spec equivalence between named classes corner case