Is bearer-of-at-some-time inverse relation at the instance level of inheres-in-at-all-times?

[GoogleCodeExporter]

Comes up in discussion of BFO 1.2 review, where they are taken as inverses.

Original issue reported on code.google.com by alanruttenberg@gmail.com on 29 Jan 2013 at 5:50

• Blocking: #165

[GoogleCodeExporter]

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)

Original comment by cmung...@gmail.com on 28 Feb 2013 at 3:35

[GoogleCodeExporter]

Original comment by cmung...@gmail.com on 24 Apr 2013 at 7:15

• Now blocking: #165

[GoogleCodeExporter]

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.

Original comment by alanruttenberg@gmail.com on 30 Apr 2013 at 10:18

[GoogleCodeExporter]

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

Original comment by alanruttenberg@gmail.com on 30 Apr 2013 at 10:32

• Added labels: Milestone-BFO2-Release

[GoogleCodeExporter]

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.

Original comment by alanruttenberg@gmail.com on 7 May 2013 at 10:01