Is bearer-of-at-some-time inverse relation at the instance level of inheres-in-at-all-times?
Opened this issue · 5 comments
From alanruttenberg@gmail.com on January 29, 2013 12:50:10
Comes up in discussion of BFO 1.2 review, where they are taken as inverses.
Original issue: http://code.google.com/p/bfo/issues/detail?id=144
From cmung...@gmail.com on February 27, 2013 19:35:33
Do these need examined on a case by case basis? Or is there a general template we can take advantage of?
I suspect the latter. E.g.
(if
(and (nonmigratory r)
(reference_inverse_of r s)
(all_times_cognate r r_all_times)
(some_times_cognate s s_some_times))
(OWLInverseObjectProperties r_all_times s_some_times))
I just threw this together. The FOL group could get to work on proving things like this.
Roughly the intuition is that there are some reference relations that are non-migratory. E.g. once you inhere in a thing, you inhere in that thing all the time you exist. You never hop off onto another bearer.
part_of is an example of a relation that could not be declared non-migratory, because stuff gets exchanged all the time (e.g. cellular material and cells, cells and tissues)
From cmung...@gmail.com on April 24, 2013 12:15:19
Blocking: bfo:165
From alanruttenberg@gmail.com on April 30, 2013 15:18:27
They need to be examined case by case, because time has shown that it is too hard for now to generalize.
To answer the question, which is the subject of the issue, I don't believe there is a sensible inverse of inheres-in-at-all-times other than inv(inheres-in-at-all-times). That's because we have two reasonable possible inverses - bearer-of-at-some-time and bearer-of-at-all-times. Whether or not one or the other obtains depends on how long the bearer lives, as well as the nature of the dependent. Charge, is borne at all times. Roles are typically borne at some times, though if the bearer is "short-lived" it can be the case that it bore the quality at all times even if it didn't need to (so to speak).
Currently, inheres-in-at-all-times has no named inverse. Bearer-of-at-all-times and Bearer-of-at-some-times are sub properties, respectively, of has-specific-dependent-at-all-times and has-specific-dependent-at-some-time.
I think we could add:
inv(bearer-of-at-all-times) subPropertyOf inheres-in-at-all-times
inv(bearer-of-at-some-time) subPropertyOf inheres-in-at-all-times
i.e. regardless of how long the dependent was borne, the dependent always inhered in the same thing (since inherence is non-migratory).
I will do so, and close the issue after a couple of weeks unless there is objection.
From alanruttenberg@gmail.com on April 30, 2013 15:32:16
added
inv(bearer-of-at-all-times) subPropertyOf inheres-in-at-all-times
inv(bearer-of-at-some-time) subPropertyOf inheres-in-at-all-times
axioms 700, 701 in next release
file specification;gcis-with-no-other-home.lisp
Labels: Milestone-BFO2-Release
From alanruttenberg@gmail.com on May 07, 2013 15:01:53
I think I've made a mistake here, determined after discussion at the BFO call.
inheres-in-at-all-times subPropertyOf inv(bearer-of-at-some-time) seems justified for sure (read subPropertyOf as implication).
Whether the reverse is true hinges on the difference between the relation of specific dependence and inherence. Since bearer of is used as the reverse relation for both, I don't think the inverse is justified. But we need some proof/counterexample.