okamžik (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.

Ontologie

SUMO / BASE-ONTOLOGY

Nadtřída(y)

entita

abstraktum

veličina

fyzikální veličina

konstantní veličina

časová míra

časová pozice

okamžik

Instance(s)

positive infinity negative infinity

Související termín(y)

časový interval

Constrains relations

begin fn end fn time interval fn where fn before before or equal temporally between temporally between or equal

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.

Axiomy (10)

časová pozice je exhaustively partitioned into časový interval,okamžik.

(partition TimePosition TimeInterval TimePoint)

Jestliže point je instancí třídy okamžik a point se nerovná positive infinity, potom point happens before positive infinity.

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

Jestliže point je instancí třídy okamžik a point se nerovná positive infinity, potom existuje otherpoint tak, že otherpoint je between point and positive infinity.

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

Jestliže point je instancí třídy okamžik a point se nerovná negative infinity, potom negative infinity happens before point.

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

Jestliže point je instancí třídy okamžik a point se nerovná negative infinity, potom existuje otherpoint tak, že otherpoint je between negative infinity and point.

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

Jestliže point je instancí třídy okamžik, potom existuje časový interval interval tak, že point je a part of interval.

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

Jestliže interval je instancí třídy časový interval, potom existuje okamžik point tak, že point je a part of interval.

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

jestliže obj je instancí třídy objekt,
potom existují okamžik time1,okamžik time2 tak, že time1 happens before time2 a pro všechny time platí: jestliže time1 happen?{s} before or at time a time happen?{s} before or at time2, potom obj exists during 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 exists during time a time je instancí třídy okamžik tehdy a jen tehdy pokud time je between or at "the beginning of doba existence phys" and "the end of doba existence phys".

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

jestliže "decomposition of interval into ? interval-types" se rovná class,
potom pro všechny time platí: jestliže time je instancí třídy okamžik a time je a part of interval, potom existuje class instance tak, že time je a part of 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))))))