temporally starts

IRI: https://spec.industrialontologies.org/ontology/construct/temporallyStarts

Defined In: https://spec.industrialontologies.org/ontology/core/Core/

Type: Object Property

Range: bfo.BFO_0000015 | bfo.BFO_0000202

Inverse Of: temporally started by

Definition

relation that holds between two intervals or processes i and j when the first instant of the temporal extent of i is the same as first the instant of the temporal extent of j and the last instant of i precedes the last instant of j

Examples

• the process of cranking temporally starts (the running of) an internal combustion engine; the pressing of a switch temporally starts (the running of) some machine; the New Year’s Day temporally starts a year.

Adapted From

• https://dl.acm.org/doi/10.1145/182.358434

Formal Axioms

First-Order Logic Axioms

LA1: temporallyStarts(i,j) → (TemporalInterval(i) ∧ TemporalInterval(j)) ∨ (Process(i) ∧ Process(j))

LA2: TemporalInterval(i) ∧ TemporalInterval(j) ∧ temporallyStarts(i,j) → ∃i1∃i2∃j1∃j2(TemporalInstant(i1) ∧ TemporalInstant(i2) ∧ TemporalInstant(j1) ∧ TemporalInstant(j2) ∧ hasFirstInstant(i,i1) ∧ hasLastInstant(i,i2) ∧ hasFirstInstant(j,j1) ∧ hasLastInstant(j,j2) ∧ occursSimultaneouslyWith(i1,j1) ∧ precedes(i2,j2))

LA3: Process(i) ∧ Process(j) ∧ temporallyStarts(i,j) → ∃i1∃j1(TemporalInterval(i1) ∧ TemporalInterval(j1) ∧ occupiesTemporalRegion(i,i1) ∧ occupiesTemporalRegion(j,j1) ∧ temporallyStarts(i1,j1))

LA4: temporallyStarts(i,j) ↔ ∃k∃l(meets(k,i) ∧ meets(k,j) ∧ before(i,l) ∧ meets(j,l))

Semi-Formal Natural Language Axioms

LA1: If i ‘temporally starts’ j then either both are ‘temporal intervals’ or both are ‘process’

LA2: If both i and j are ‘temporal intervals’ and i ‘temporally starts’ j then the ‘first instant’ of i ‘occurs simultaneously with’ the ‘first instant of’ j and the ‘last instant of’ i ‘precedes’ the ‘last instant of’ j

LA3: If both i and j are ‘process’ and i ‘temporally starts’ j then the ‘temporal interval’ that i occupies ‘temporally starts’ the ‘temporal interval’ that j occupies

LA4: i ‘temporally starts’ j if and only if there exists k that ‘meets’ i and j and there exists l such that i is ‘before’ l and j ‘meets’ l

Description Logic

domain: bfo:process ⊔ bfo:temporal_interval

range: bfo:process ⊔ bfo:temporal_interval

inverse: constr:temporallyStartedBy

Transitive

domain: bfo:process or bfo:temporal_interval

range: bfo:process or bfo:temporal_interval

inverse: constr:temporallyStartedBy

Transitive