Examples

Other relations

This relation has no inverse relations declared

id	OBO_REL_I:0000041
name	occurs_at
properties
aliases
anti_symmetric
holds_between	occurrent and temporal_instant
reflexive
symmetric
transitive
all_some_in_reference_context
example

Axioms for this relation:

axiom

occurs_at( p, t) ↔ ∃ c[ has_participant( p, c, t) ]

Axioms that refer to this relation:

axiom	preceded_by( p, p1) ↔ occurs_at( p, t) ∧ occurs_at( p1, t1) → earlier_than( t1, t)
axiom	first_instant_of( t, p) ↔ occurs_at( p, t) ∧ earlier_than( t1, t) → ¬ ( occurs_at( p, t1) )
axiom	last_instant_of( t, p) ↔ occurs_at( p, t) ∧ earlier_than( t, t1) → ¬ ( occurs_at( p, t1) )
axiom	Axiom: p has_duration y iff p is an occurrent, and for any t such that t is bound by the start and end of p, it is the case that p occurs_at t, and y is the interval with those boundaries has_duration( p, y) ↔ instance_of( p, occurrent) ∧ ∃ t1[ first_instant_of( t1, p) ] ∧ ∃ t2[ last_instant_of( t2, p) ] ∧ earlier_than( t1, t) ∧ earlier_than( t, t2) → occurs_at( p, t) ∧ y = interval( t1, t2)