Spreadsheet errors, and relations absent from OWL files

[CDowland]

This concerns the spreadsheet and csv files for the terms, as well as the OWL files, within the folder 21838-2. In the csv and Excel spreadsheet labeled “bfo-2020-terms,” there are errors in which some of the symbols appear as a superscript “3” instead of what they’re suppose to be. I'm attaching a picture that shows an example of this.

For most of these, the correct version can be found in the OWL file(s) for BFO 2020. However, the definition of member part of contains such an error, and neither it nor has member part appear in either bfo-2020.owl or bfo-2020-without-some-all-times.owl.

I have 3 related questions/requests:

1. Could corrected versions of "bfo-2020-terms" be made available?
2. Could member part of and has member part be added to one or both OWL files; or if there is a reason why they were intentionally left out, could that reason be shared here?
3. Could someone please reply with the corrected version of the error that appears in the definition of member part of, which is within the red rectangle in the image above? Based on the temporalized versions of the relation, I assume the corrected version would read "n ≠ 1," but confirmation would be appreciated.

Thank you.

[hoganwr]

I would think re: #3 it should be n > 1 or n >= 1

On Mon, Aug 7, 2023 at 10:35 PM Clint Dowland @.***> wrote:

This concerns the spreadsheet and csv files for the terms, as well as the OWL files, within the folder 21838-2 https://github.com/BFO-ontology/BFO-2020/tree/master/21838-2. In the csv and Excel spreadsheet labeled “bfo-2020-terms,” there are errors in which some of the symbols appear as a superscript “3” instead of what they’re suppose to be. I'm attaching a picture that shows an example of this.

[image: member part of def] https://user-images.githubusercontent.com/52045818/258974603-74f88edb-baa4-4f16-99df-3a6a5dcfacd5.png

For most of these, the correct version can be found in the OWL file(s) for BFO 2020. However, the definition of member part of contains such an error, and neither it nor has member part appear in either bfo-2020.owl or bfo-2020-without-some-all-times.owl.

I have 3 related questions/requests:

1. Could corrected versions of "bfo-2020-terms" be made available?
2. Could member part of and has member part be added to one or both OWL files; or if there is a reason why they were intentionally left out, could that reason be shared here?
3. Could someone please reply with the corrected version of the error that appears in the definition of member part of, which is within the red rectangle in the image above? Based on the temporalized versions of the relation, I assume the corrected version would read "n ≠ 1," but confirmation would be appreciated.

Thank you.

— Reply to this email directly, view it on GitHub https://github.com/BFO-ontology/BFO-2020/issues/69, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAJR55VPFDUHTOGNRUJ4QXLXUGXXVANCNFSM6AAAAAA3H2XBGE . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[CDowland]

@hoganwr That's what I assumed at first as well, but then I noticed that the corresponding portions of the temporalized versions have "n ≠ 1" (in the OWL files).

[alanruttenberg]

Thanks for the report. The subscript 3 was presumably a copy/paste character encoding problem when the excel file was created, since it's in the Excel and so that needs to be fixed as well.

Regarding "member part of" for OWL, the relations would be "member part of at some time" and "member part of at all times", because "member part of" is time indexed, and OWL has only binary relations. Those relations are in bfo-2020.owl but not bfo-2020-without-some-all-times.owl

@hoganwr it should probably be n>=1 rather than n ≠ 1, but with a proviso that there is some t when n>1. We allow object aggregates to temporarily have a single member. This is because organizations are typically represented (for better or worse) as object aggregates, and organizations can temporarily have a single member. Looks like the elucidation of object aggregate should reflect that too. Elucidations and definitions are Barry's job to craft, so I'll forward this issue to him asking for corrections.

[johnbeve]

@alanruttenberg Barry and I were incidentally refining the definitions/elucidations a couple of weeks ago and crafted some updates. Will post here for review.

[hoganwr]

Great! I was thinking same thing: it should be that at some time t, n > 1, and it is permissible that at other times t, there is only 1. I assumed character encoding error as well, but saw the superscript 3 in the CSV file, without considering that the CSV was generated by Excel. Crazy that in 2023 we still have character encoding problems.

On Tue, Aug 8, 2023 at 6:42 PM John Beverley @.***> wrote:

@alanruttenberg https://github.com/alanruttenberg Barry and I were incidentally refining the definitions/elucidations a couple of weeks ago and crafted some updates. Will post here for review.

— Reply to this email directly, view it on GitHub https://github.com/BFO-ontology/BFO-2020/issues/69#issuecomment-1670452690, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAJR55QGYFGCKWUTJTFW62DXULFFTANCNFSM6AAAAAA3H2XBGE . You are receiving this because you were mentioned.Message ID: @.***>

[CDowland]

I should clarify that I’m not just raising this question for potential improvements, but also because I want to quote the definition in its current form. So when I ask what the superscript 3 was meant to be, I’m not asking what’s the best thing to put there. Instead I’m asking what would be there currently if not for the encoding error (which might be different from what’s best).

[alanruttenberg]

@CDowland the superscript 3 is in place of "≠" (not equals) in the original definition.

[CDowland]

Thanks!

[johnbeve]

@alanruttenberg Barry and I were incidentally refining the definitions/elucidations a couple of weeks ago and crafted some updates. Will post here for review.

Suggested revisions to member part of some/all times object properties:

• b member part of c at all times =_Def for all times t, b exists at t implies (b is an object & c is an object aggregate & there is at t a mutually exhaustive and pairwise disjoint partition of c into object(s) x₁...x_n such that b=x_i for some 1≤ i ≤ n)

• b member part of c at some time =_Def for some time t (b is an object & c is an object aggregate & there is at t a mutually exhaustive and pairwise disjoint partition of c into object(s) x₁...x_n such that b=x_i for some 1≤ i ≤ n)

WIP (currently ambiguous between OWL and FOL) suggestion for revising elucidation of object aggregate:

• c is an object aggregate =_Def c is a material entity & there exist times t₁ ≠ t₂ & objects x₁...x_n (for 1< n) such that each x_i (for 1< i ≤ n) is a member part of c at t₁ & there are objects x₁...x_m (for 1≤ m) such that each x_k (for 1≤ k ≤ m) is a member part of c at t₂

In words, c is an object aggregate just in case it's a material object and at some time it has at least two object member parts and at a distinct time it has at least one object member part.

Barry suggested we should add that for any t most of the member parts at t are still member parts at either or both of t+δt and at t-δt. My (first pass) suggestion is to add to the elucidation of object aggregate the clause:

• for any t₃ ≠ t₄ there is some z such that z is a member part of c at t₃ & z is a member part of c at t₄ & t₃ precedes t₄

Which doesn't capture 'most' and doesn't enforce t₃ immediately precedes t₄. More soon.

[alanruttenberg]

Quick thoughts: 1) Usually the all/some time relations don't have separate definitions, instead relying on the time indexed relations. 2) The t+/- delta is problematic because we don't have density and we don't have immediately precedes for temporal instants, though it's possible to define it (with a technical issue to deal with) for intervals. Temporal quantification is over temporal regions, not temporal instants. This issue alone merits a review of definitions.

Maybe more comments later.

[alanruttenberg]

I've been meaning to write up how to think about time in the BFO-2020 axiomatization, so here's a go.

For any relation temporally indexed, the temporal index ranges over all temporal-regions. Temporal regions include instants and intervals, but can also be disjoint sets of them.

Suppose you asserted just an interval i1 and some instant p1 inside it. One axiom specifies that every temporal region has a first and last time point. It is not implied that the first and last time point are part of the interval. Another axiom (or 2 can't recall) specify that there is an interval between any two instants that don't have an instant between them. Finally another axiom asserts that any temporal region that is within(*) the first or last instant of an interval is part of that interval. So our initial assertion of i1 and p1 would land up with a model:

           i1
----------------------- 
|           |         |
f1         p1        l1
------------ ----------
    i2          i3 

*: Withing means the first instant of the included is-preceded-by the first instant of the includer and the last instant of the included precedes the last instant of the includer.

In the above, f1 is the implied first instant of i1 and l1 is the implied last instant of i1. p1 is part of i1. i2 is the implied interval between f1 and p1 (which serves as it's last instant) and i3 is the implied interval between p1 (which serves as it's first instant) and l1. i2 and i3 are each part of i1.

So when you say "forall t" you mean i1,i2,i3,f1,p1,l1.

Suppose you want to assert something like a permanent generic r - instances of class C1 have "at all times" exactly one instance of class C2 related by r, but not necessarily the same one. You have to be careful.

The cardinality constraint is written

(forall (c1 c2 c3 t)
  (implies (and (r c1 c2 t) (r c1 c3 t))
     (= c2 c3)))

(note that if r can't be transitive for the above - it's more complicated in that case, because you probably want to say something like r is "direct" part of)

You can't write the permanent generic axiom like this, as you would if you were quantifying over instants.

(forall (t c1)
  (implies (C1 c1 t)
    (exists (c2) 
      (and (C2 c2 t) 
       (r c1 c2 t)))))

Here's why:

Suppose cx1 is always an instance of C1.

One of the values of t will be i1 and so there will be some cx2 instance of C2 such that (r cx1 cx2 i1)

Most relations such as r are dissective wrt t, namely if (r x y t) and (part-of t' t) then (r x y t'). Makes sense since if you say something is true between noon and 1pm then the same thing will typically be true between 12:05 and 12:10pm.

So now there's no chance for there to be another cx3 instance of C2 such that (r cx1 cx3 ) where cx3 is not equal to cx2, and is any of the other temporal regions, since they are all part of i1 and asserting the above will have it be the case that there would be 2 values for the second relata. For any part of i1, we'll have (r cx1 cx2 ) inferred by the dissective axiom if it's the case that (r cx1 cx3 ), because of the one-value axiom we'll infer (= cx2 cx3). Therefore where we intended permanent generic, we actually land up with permanent specific.

I think the general work around is to write it as such:

(forall (t c1)
  (implies (C1 c1 t)
    (exists (c2 t') 
      (and (temporal-part-of t' t)
       (C2 c2 t')
       (r c1 c2 t')))))

Now we're good because it won't have to be the case that (r cx1 cx2 i1) because it can be the case that there's some t' part of t1 where (r cx1 cx2 t'. The effect of this will be that the only temporal regions that "matter" are the ones with no part: f1,i2,p1,i3,l1. Together those "cover" all times in the sense we intend. I think that will generally be true so the "part-of" workaround will work in general, though I should really prove it.

Bottom line: Be careful about what you say when quantifying over all t, and be especially careful when there are two times mentioned, as is done in the WIP in https://github.com/BFO-ontology/BFO-2020/issues/69#issuecomment-1681036994 . I'm not saying it doesn't work, just that you need to think carefully about whether it does.