search

BFO-ontology / BFO-2020

A repository for BFO 2020 artifacts specified in ISO 21838-2:2020
70 stars 27 forks source link

show that the bearer of an sdc/gdc must participate in a process #38

Open wdduncan opened 2 years ago

wdduncan commented 2 years ago

@alanruttenberg Following up on this COB issue.

The domain of the participates in relations are sdc, gdc, or ic but not spatial region. Together with the axioms that there must be a participant and that sdc and gdc participants imply a bearer participates, and bearers are material, one would conclude that it must be a material entity. When I'm next doing that sort of thing, I'll try to show it's provable.

These two CL axioms seem to prove this: SDC, GDC

Are you going to show how to run the theorem prover that uses the CL files?
Should object property chain be created in the OWL version that reflects this?

alanruttenberg commented 2 years ago

There isn't a theorem prover that takes the CL yet, that I know of. HETS has one but last I checked it was for the previous version of the CL spec. The CL is generated from an idiosyncratic dialect of CLIF somewhere in my logic software. Generally I translate to SMT-LIB syntax for use with vampire or Z3 and to prover9 syntax when using prover9.

However, there is a prover9 version of the axioms so you could use prover9 to try the proof.

Haven't thought about this for a while. What's the specific property chain you are thinking of?

wdduncan commented 2 years ago

What's the specific property chain you are thinking of?

I think the property that would be needed:

'bearer of' o 'participates in'
alanruttenberg commented 1 year ago

There's no 'participates in' in BFO-2020. I think 'bearer of' o 'participates in at all times' < 'participates in at some time' and maybe
'bearer of' o 'participates in at some time' < 'participates in at some time'. The all-times all-times version probably not because the SDC participation axiom is weak. It only say that if the SDC participates then the bearer must participate some of that time. We could have a discussion of whether that's too weak. At the moment I'm trying to prove the above but am failing. I typically have to choose which axioms to try to do the proof with because using all of them causes the reasoner to time out. Will keep trying.

wdduncan commented 1 year ago

There's no 'participates in' in BFO-2020.

Yes, there is not (at least in the OWL version). Sorry, I wasn't more careful.

In the OWL version, the range of bearer of is an SDC. I cannot think of counter example in which an SDC participates in a process, but its bearer does not. That is, this seems to hold:

'bearer of'  o 'participates in at some time' < 'participates in at some time'

The range of the more general relation 'specifically depended on by' is also an SDC. But since its domain is broader ((SDC or IC) and (not SR)), it is more difficult to think/reason about.

However in the case of a GDC, it seems to me that is carrier of at some time is too weak. An IC may bear a GDC at a different time than when the IC participates in the process (e.g., the GDC has migrated to different bearer). I think is carrier of at all times still holds, though. That is:

'is carrier of at all times' o 'participates in at some time' < 'participates in at some time'

We should probably also think about property chains that hold for has participant at some/all time(s) too.

Happy to discuss further ...