Pattern for defining temporalized relations in terms of references

[GoogleCodeExporter]

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 reported on code.google.com by cmung...@gmail.com on 5 Mar 2013 at 7:57

[GoogleCodeExporter]

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. 

Original comment by cmung...@gmail.com on 12 Mar 2013 at 12:28

[GoogleCodeExporter]

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))

Original comment by cmung...@gmail.com on 12 Mar 2013 at 12:34

[GoogleCodeExporter]

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? 

Original comment by steschu@gmail.com on 12 Mar 2013 at 11:07

[GoogleCodeExporter]

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.

Original comment by alanruttenberg@gmail.com on 12 Mar 2013 at 3:56

• Changed state: Accepted

[GoogleCodeExporter]

"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.

Original comment by dosu...@gmail.com on 12 Mar 2013 at 7:49

[GoogleCodeExporter]

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

Original comment by alanruttenberg@gmail.com on 12 Mar 2013 at 9:54

[GoogleCodeExporter]

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. 

Original comment by alanruttenberg@gmail.com on 13 Mar 2013 at 1:28

[GoogleCodeExporter]

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.

Original comment by alanruttenberg@gmail.com on 19 Mar 2013 at 10:28