I am fairly sure the property chain declarations in the current BFO2 ontology are incomplete.
E.g. I think there should be
InverseOf(continuant-part-of-at-all-times) o has-continuant-part-at-some-time -> has-continuant-part-at-some-time
This is equivalent to writing
has-continuant-part-at-all-times-that-part-exists o has-continuant-part-at-some-times -> has-continuant-part-at-some-times
I have not yet managed to generate a proof of this. My attempts so far are in the examples/property-chains/ directory.
It would be good if there were some kind of annotation assertion that allowed us to know if the OP was considered "done" - i.e. absence of an axiom is deliberate rather than error of omission.
From cmung...@gmail.com on March 17, 2013 14:16:55
I am fairly sure the property chain declarations in the current BFO2 ontology are incomplete.
E.g. I think there should be
This is equivalent to writing
I have not yet managed to generate a proof of this. My attempts so far are in the examples/property-chains/ directory.
It would be good if there were some kind of annotation assertion that allowed us to know if the OP was considered "done" - i.e. absence of an axiom is deliberate rather than error of omission.
Original issue: http://code.google.com/p/bfo/issues/detail?id=160