zhengj2007 / bfo-export

Automatically exported from code.google.com/p/bfo
0 stars 0 forks source link

exists_at treatment #48

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
(mind the two uses of exists - exists( , ) is the relation, and exists without 
parentheses is the logical exists.)

Should it not be the case that for any categorical continuant predicate we have 
an axiom of the form: 

forall t instantiates(x,cat,t) -> exists(x,t)

and for the rigid categories (most of BFO, other than subkinds of material 
entity?)

if there exists some t1 st. instantiates(x,cat,t1) then forall t exists(x,t) -> 
instantiates(x,cat,t)

and for occurrents:

occurrent(x) -> exists t projects_onto(x,t) and forall t,  t1 part_of t -> 
exists_at(x,t) 

and for time-dependent relations

r(x,y,t) -> exists(x,t), exists(y,t)

and for time independent relations

r(x,y)

not(exists(x,t)) or (not(exists(x,t)) -> not(r(x,y))

I don't know what to do about time itself, which is in the domain of discourse, 
and so can be predicted with exists_at

Original issue reported on code.google.com by alanruttenberg@gmail.com on 24 May 2012 at 12:17

GoogleCodeExporter commented 9 years ago
So far there is no axiom using this relation or its inverse. What about the 
axiom
continuant subClassOf exists_at some temporal_region ?

Original comment by steschu@gmail.com on 8 Jul 2012 at 9:32