obophenotype / uberon

An ontology of gross anatomy covering metazoa. Works in concert with https://github.com/obophenotype/cell-ontology
http://obophenotype.github.io/uberon/
Other
128 stars 28 forks source link

Document mereological sum design pattern #3181

Open cmungall opened 5 months ago

cmungall commented 5 months ago

We have some old documentation for part-disjointness: https://github.com/obophenotype/uberon/wiki/Part-disjointness-Design-Pattern

This needs translated to yaml

However, we have no documentation for the mereological sum DP

These are stored in the disjoint_union_over.ofn component:

The basic idea was to encode mereological sum axioms. These are conceptually very straightforward

W = P1 + P2 + ... + Pn

These were translated into two axioms:

  1. (part-of some W) = (part-of some P1) or ... (part-of some Pn)
  2. Disjoint( (part-of some P1), ..., (part-of some Pn))

And actually to be complete this needs expanded further to account for the local reflexivity of part-of in the context of this.

However, expansion 1 above is actually wrong; consider

NS = CNS + PNS

If we expand to:

`(part-of some NS) = (part-of some CNS) or (part-of some PNS)

This is not right, because a structure that was within the NS as a whole but overlapped CNS and PNS

What we in fact need to write is

(grain and part-of some NS) = (grain and part-of some CNS) or (grain and part-of some PNS)

(expansion 2 is fine)

Where grain is something small enough that it doesn't span a boundary. cell is not safe since some cells span both parts (in particular any projecting neuron). atom is safe. At this point the axiom ceases to be useful...

I am not sure what the action is for this issue - it may be simplest if we don't try and represent msums at all and just focus on spatial disjointness. But I at least wanted to record some of the original thinking.

gouttegd commented 5 months ago

I am not sure what the action is for this issue

If I understand correctly, it could be that at least some of the type 1 expansions are correct?

Given W = P1 + P2 + ... + Pn, if (a) there is no structure that is part of W while overlapping several of the Pn components (which, I agree, is clearly not the case of the “CN = PNS + CNS” case), and (b) assuming the sum is “complete” (it lists all the components that make up W, without missing any), then the following equivalence is still correct:

(part-of some W) EquivalentTo (part-of some P1) or (part-of some P2) or ... (part-of some Pn)

So maybe we should review every sum in disjoint_union_over (there’s something like two dozens of them), see if they meet the two criteria (a) and (b) above, and for those that do not (including those for which we are not sure that they meet the criteria, e.g. if if we are not sure that there can’t be a structure overlapping several parts), we remove the type 1 expansion.

gouttegd commented 5 months ago

Here are the “type 1” axioms in disjoint_union_over.