Pattern for defining temporalized relations in terms of references

[zhengj2007]

From cmung...@gmail.com on March 05, 2013 14:57:40

The release notes say:

" We use two patterns exemplified in the next two definitions:

x rel-at-some-time y -> exists(t) exists_at(x,t) -> exists_at(y,t) and rel(x,y,t)

x rel-at-all-times y -> forall(t) exists_at(x,t) -> exists_at(y,t) and rel(x,y,t) "

If these are definitions, then the outer implicational arrows should be bidirectional.

The FOL group could help with some of the necessary proofs here. But in the interim the OWL docs could be updated (ideally there would be a living document for some of this, the Graz release notes can't be updated).

Some of the documentation could do directly in the OWL.

I would prefer to see the full FOL for each definition in the OWL, rather than the the RHS of the above axiom, as it is currently.

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

[zhengj2007]

From cmung...@gmail.com on March 11, 2013 17:28:11

Further comment / request for clarification on the -at-some-time variant from Fabian:

---

Chris and I have been discussing the temporal relations in the BFO 2 OWL release notes. It says that you are using the following definition pattern

x rel-at-some-time y -> exists(t) exists_at(x,t) -> exists_at(y,t) and rel(x,y,t)

It seems to me not to capture what you want. First of all it is not a definition (since it is an "if ... then" not an "if and only if"), but even if I read it as definition, it has odd consequences. E.g., something that does not exist at all times is part-at-some-time of everything else. .

Are you sure you don't mean (using prefix notation and parenthesis for clarity):

 (iff 
      (rel-at-some-time x y) 
      (exists (t)
            (and 
                 (exists_at x t) 
                 (exists_at y t)
                 (rel x y t) 
                ))))

Or in English: x is part at some time of y is defined as there is a time when both exist and at that time x is part of y.

[zhengj2007]

From cmung...@gmail.com on March 11, 2013 17:34:04

There may actually be a simpler pattern:

(iff 
      (rel-at-some-time x y) 
      (exists (t) (rel x y t)))

Assuming some "realist" supplementary axioms at the FOL level that say things like:

(if (rel x y t) (exists_at x t))

[zhengj2007]

From steschu@gmail.com on March 12, 2013 04:07:49

I would say that

 (iff 
      (rel-at-some-time x y) 
      (exists (t)
            (and 
                 (exists_at x t) 
                 (exists_at y t)
                 (rel x y t) 
                ))))

is most in line with BFO2. Wasn't it planned to include the temporalized relations into he BFO2 reference?

[zhengj2007]

From alanruttenberg@gmail.com on March 12, 2013 08:56:24

The plan was to include them, but Barry asked that he first get the reference without them settled. I had been expecting him to make another bolus of changes, but it seems that has been delayed by other priorities of his. We should inquire, or get some folks on the line for doing the work.

I believe that the IFF is preferred, if we include in the FOL a literal translation of the OWL relation. However it is worth considering whether that is in fact what we will do. The alternative is that the path from OWL to FOL is template expansion in which the consequent is substituted for the OWL relation. The idea of a "BFO2 reading of the OWL", at least as I imagine it, contemplates such substitutions as the mechanism. We don't reason with some FOLifiied OWL - rather we translate the OWL to FOL.

Now maybe someone can show these are exactly the same, or that we lose something if we take that approach.

Status: Accepted

[zhengj2007]

From dosu...@gmail.com on March 12, 2013 12:49:13

"We don't reason with some FOLifiied OWL - rather we translate the OWL to FOL." Perhaps I'm misunderstanding but isn't the FOL the primary reference? It seems odd to me to use the weaker language as the reference to be translated from.

[zhengj2007]

From alanruttenberg@gmail.com on March 12, 2013 14:54:57

the reference is what we do the full reasoning in. So it is perfectly natural to take other languages and translated them to FOL for verification

[zhengj2007]

From alanruttenberg@gmail.com on March 13, 2013 06:28:50

Fabian's observation is correct, thanks. I will adjust the documentation and build accordingly, and also address Chris' documentation request in the originally posted issue. FWIW, I used the SNARK theorem prover to convince myself and to start getting my chops.

[zhengj2007]

From alanruttenberg@gmail.com on March 19, 2013 15:28:31

https://bfo.googlecode.com/svn/trunk/src/ontology/owl-group/tests/test-issue-154.snark - a test to validate the problem using snark. Includes a reformulation of the problem after talking to Fabian.