A primitive relation between a continuant and an instant of time.

Examples

Other relations

This relation has no inverse relations declared

id	OBO_REL_I:0000040
name	exists_at
properties
aliases
anti_symmetric
holds_between	continuant and temporal_instant
reflexive
symmetric
transitive
all_some_in_reference_context
example
text_definition	A primitive relation between a continuant and an instant of time.

Axioms for this relation:

axiom	Axiom: something exists at a time iff it is participating in something at that time exists_at( c, t) ↔ ∃ p[ has_participant( p, c, t) ]
axiom	Axiom: something exists at a time iff it is an instance of something at that time exists_at( i, t) ↔ ∃ U[ instance_of( i, U, t) ]

Axioms that refer to this relation:

axiom	only_exists_prior_to( c, t) ↔ ∃ t1[ exists_at( c, t1) ∧ earlier_than( t1, t) ] ∧ exists_at( c, t2) → earlier_than( t, t2)
axiom	only_exists_subsequent_to( c, t) ↔ ∃ t1[ exists_at( c, t1) ∧ earlier_than( t, t1) ] ∧ exists_at( c, t2) → earlier_than( t2, t)
axiom	exists_at( x, t) ∧ ∀ z[ overlaps( z, x, t) → overlaps( y, x, t) ] → part_of( x, y, t)
axiom	part_of( x, y, w) → exists_at( x, w) ∧ exists_at( y, w)