時點 (TimePoint)

An extensionless point on the universal timeline. The TimePoints at which Processes occur can be known with various degrees of precision and approximation, but conceptually TimePoints are point-like and not interval-like. That is, it doesn't make sense to talk about what happens during a TimePoint, or how long the TimePoint lasts.

Ontology

SUMO / BASE-ONTOLOGY

Superclass(es)

實體

抽象的

數量

物理量

常量

時間單位

時間

時點

Instance(s)

時間終點/永遠時間起點/亙古

Coordinate term(s)

時段

Constrains relations

（時間）開始函數（時間）結束函式時間歷程函數位置函數先於先於或同時時間介於時間介於或同時

Related WordNet synsets

point, point in time: a very short period of time; "at that point I had to leave"

See more related synsets on a separate page.

Axioms (10)

時間完全分割成時段,時點.

(partition TimePosition TimeInterval TimePoint)

If point 是時點的實例 and point 等於時間終點/永遠, then point (沒) 發生?{s} 在時間終點/永遠之前.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT PositiveInfinity)))
      (before ?POINT PositiveInfinity))

If point 是時點的實例 and point 等於時間終點/永遠, then there exists otherpoint so that otherpoint 在 point 和時間終點/永遠之間 .

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT PositiveInfinity)))
      (exists
            (?OTHERPOINT)
            (temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))

If point 是時點的實例 and point 等於時間起點/亙古, then 時間起點/亙古 (沒) 發生?{s} 在 point 之前.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT NegativeInfinity)))
      (before NegativeInfinity ?POINT))

If point 是時點的實例 and point 等於時間起點/亙古, then there exists otherpoint so that otherpoint 在時間起點/亙古和 point 之間 .

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT NegativeInfinity)))
      (exists
            (?OTHERPOINT)
            (temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))

If point 是時點的實例, then there exists 時段 interval so that point 是 interval 的部分.

(=>
      (instance ?POINT TimePoint)
      (exists
            (?INTERVAL)
            (and
                  (instance ?INTERVAL TimeInterval)
                  (temporalPart ?POINT ?INTERVAL))))

If interval 是時段的實例, then there exists 時點 point so that point 是 interval 的部分.

(=>
      (instance ?INTERVAL TimeInterval)
      (exists
            (?POINT)
            (and
                  (instance ?POINT TimePoint)
                  (temporalPart ?POINT ?INTERVAL))))

if obj 是物體的實例,
then there exist 時點 time1,時點 time2 so that time1 (沒) 發生?{s} 在 time2 之前 and for all time holds: if time1 (沒) 發生?{s} 在 time 或之前 and time (沒) 發生?{s} 在 time2 或之前, then obj (不) 存在s time 期間

(=>
      (instance ?OBJ Object)
      (exists
            (?TIME1 ?TIME2)
            (and
                  (instance ?TIME1 TimePoint)
                  (instance ?TIME2 TimePoint)
                  (before ?TIME1 ?TIME2)
                  (forall
                        (?TIME)
                        (=>
                              (and
                                    (beforeOrEqual ?TIME1 ?TIME)
                                    (beforeOrEqual ?TIME ?TIME2))
                              (time ?OBJ ?TIME))))))

phys (不) 存在s time 期間 and time 是時點的實例 if and only if time 在 ""phys 存在的時間" 的 �}始" 和 ""phys 存在的時間" 的結束" 或之間 .

(<=>
      (and
            (time ?PHYS ?TIME)
            (instance ?TIME TimePoint))
      (temporallyBetweenOrEqual
            (BeginFn
                  (WhenFn ?PHYS))
            ?TIME
            (EndFn
                  (WhenFn ?PHYS))))

if "interval 分解成 ? interval-types" 等於 class,
then for all time holds: if time 是時點的實例 and time 是 interval 的部分, then there exists class instance so that time 是 instance 的部分

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME)
            (=>
                  (and
                        (instance ?TIME TimePoint)
                        (temporalPart ?TIME ?INTERVAL))
                  (exists
                        (?INSTANCE)
                        (and
                              (instance ?INSTANCE ?CLASS)
                              (temporalPart ?TIME ?INSTANCE))))))