BFO2 is less effective at error-checking than alternate approaches

[zhengj2007]

From cmung...@gmail.com on March 09, 2013 15:44:00

For examples see the OWL, screenshots and README in: https://code.google.com/p/bfo/source/browse/trunk/src/ontology/owl-group/examples/spatial-disjointness Basic summary:

RO only requires one axiom for effective checking of spatial disjointness violations:

[1](part_of some mitochondrion) DisjointWith (part_of some nucleus)

These axioms have been very useful for error checking in GO and anatomy ontologies. I have taught this pattern in courses and workshops.

There is no general recipe for translating these to BFO2. In this example I find that to approximate the same entailments it is necessary to translate this to 4 axioms:

[2] 'part of continuant at all times' some mitochondrion DisjointWith 'part of continuant at all times' some nucleus
[3] 'part of continuant at all times' some mitochondrion DisjointWith 'part of continuant at all times that whole exists' some nucleus
[4] 'part of continuant at all times that whole exists' some mitochondrion DisjointWith 'part of continuant at all times that whole exists' some nucleus
[5] 'part of continuant at all times' some nucleus DisjointWith 'part of continuant at all times that whole exists' some mitochondrion

Simply doing [2] alone is insufficient (see examples).

I think we would all agree this is far from desirable.

And the FOL reading is still short of what is intended.

Original issue: http://code.google.com/p/bfo/issues/detail?id=156

[zhengj2007]

From cmung...@gmail.com on March 09, 2013 18:36:30

One partial workaround for this would be to introduce yet another temporalized form, at-all-times-for-either-subject-or-object, and use this in the GCI. But this isn't very satisfactory from a user point of view. And the FOL is still too weak.