has_participant_at_all_time inverse property

[GoogleCodeExporter]

seems to me that participates_in_at_all_times should be asserted as inverse

Original issue reported on code.google.com by mcour...@gmail.com on 27 Jun 2012 at 10:50

[GoogleCodeExporter]

I think:

InverseProperties(
  participates_in_at_all_times
  has_participant_at_some_times
)

in general, if the 4d projection of the relation is to part_of_at_all_times 
then the inverse should be the corresponding relation that projects to 
has_part_at_some_times)

I'm guessing the proof for this shouldn't be hard, but I haven't tried.

Original comment by cmung...@gmail.com on 27 Jun 2012 at 11:06

[GoogleCodeExporter]

You're right. inverse(has_participant_at_some_times) and 
participates_in_at_some_time are currently super properties in the file 

I just realized that in several cases when creating the inverses only the 
top-property gets one (see similar issue at 
http://code.google.com/p/bfo/issues/detail?id=74) Maybe a bug in their 
automated generation?

Original comment by mcour...@gmail.com on 27 Jun 2012 at 11:25

[GoogleCodeExporter]

Re: InverseProperties(
  participates_in_at_all_times
  has_participant_at_some_times
)

No. participates_in_at_all_times ->  has_participant_at_some_times but 
has_participant_at_some_times /-> participates_in_at_all_times

Counterexample: 

Process lasts noon - 6pm.
foo exists between 2 and 4 pm.
foo participates in process from 2 to 3 pm.

Therefore 
process has_participant_at_some_times foo
but
not: foo participates_in_at_all_times process

Original comment by alanruttenberg@gmail.com on 28 Jun 2012 at 3:50

[GoogleCodeExporter]

propose that this be closed as invalid

Original comment by alanruttenberg@gmail.com on 28 Jun 2012 at 3:51

[GoogleCodeExporter]

Alan you're quite right, apologies for the noise.

Original comment by cmung...@gmail.com on 28 Jun 2012 at 3:57

[GoogleCodeExporter]

Few comments:
(1) is there any disagreement on the original tracker submission, 
participates_in_at_all_times should be asserted as inverse of 
has_participant_at_all_time? If none, this should be fixed and the tracker 
closed as fixed.
(2) I agree for the other relation, read it too fast. I think it is 
inverse(participates_at_some_times) - which is already  inferred as super 
property as mentioned in my reply so no fix needed there
(3) I would like to add an editor note that in participates_in_at_all_times, 
all_times refers to "all times that the continuant exists_at" rather than 
"all_times than the process spans" - I think having the textual human 
explanation would be a bit more readable. Objections?
(4) I would also like to add Alan's explanation above as note.

Original comment by mcour...@gmail.com on 28 Jun 2012 at 4:44

[GoogleCodeExporter]

[deleted comment]

[GoogleCodeExporter]

[note: deleted comment 7 and replaced with this one - needed adjustment]
(1) There is disagreement. Here is a counterexample - is similar to the case in 
comment 3:

Process lasts noon - 6pm.
foo exists between 2 and 4 pm.

if foo participates_in_at_all_times process, then the relation holds for all 
times when foo exists, i.e. between 2 and 4pm.
If Process has_participant_at_all_times foo, then the relation holds for all 
times when process exists, i.e. between noon and 6pm.
But foo doesn't exist between noon and 2pm or between 4pm and 6pm.

(2) Having trouble parsing. Let's discuss tomorrow. 

(3) There is a editor note (on all the 'at all times' relations) already 
present: "Alan Ruttenberg: This is a binary version of a ternary time-indexed, 
instance-level, relation. The BFO reading of the binary relation 'has 
participant at all times' is: forall(t) exists_at(x,t) -> exists_at(y,t) and 
'has participant(x,y,t)'" Did you not notice that one? Or did you read it and 
think it needs to be clearer.  There is a variant of this note one all 'at some 
times' relations.

(4) We can add it to the has-participant relation, but it is relevant for all 
the at-all-times relationships. Can we augment the note above so that it is 
applicable to all the relations? After you read, understand, and if you agree 
with the explanation, can you suggest how we can document it in such a note? 

Original comment by alanruttenberg@gmail.com on 29 Jun 2012 at 3:06

[GoogleCodeExporter]

OK - I think I see the difference now.

You say: There is disagreement. Here is a counterexample - is similar to the 
case in comment 3:

Process lasts noon - 6pm.
foo exists between 2 and 4 pm.

if foo participates_in_at_all_times process, then the relation holds for all 
times when foo exists, i.e. between 2 and 4pm.
If Process has_participant_at_all_times foo, then the relation holds for all 
times when process exists, i.e. between noon and 6pm.
But foo doesn't exist between noon and 2pm or between 4pm and 6pm.

I would suggest to use explicit names for relations to make my issue more 
obvious. We agreed previously that when we say "foo 
participates_in_at_all_times process" what we mean is "foo 
participates_in_at_all_times_foo_exists process". The inverse of which would be 
"process has_participant_foo_at_all_times_foo_exists" (inv#1) rather than 
"process has_participant_foo_at_all_times_process_exists" (inv #2) In your 
case, the all_times in has_participant suddenly refers to the process rather 
than the continuant when doing the inverse.

I don't understand why we chose to declare inv#2 in the file, while it seems 
inv#1 is the correct one to generate?

Original comment by mcour...@gmail.com on 29 Jun 2012 at 4:41