BFO2 is less effective at error-checking than alternate approaches

[GoogleCodeExporter]

For examples see the OWL, screenshots and README in:

http://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 reported on code.google.com by cmung...@gmail.com on 9 Mar 2013 at 8:44

[GoogleCodeExporter]

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.

Original comment by cmung...@gmail.com on 10 Mar 2013 at 2:36