ZeitlicheAufbauFn (TemporalCompositionFn)

The basic Function for expressing the composition of larger TimeIntervals out of smaller TimeIntervals. For example, if ThisSeptember is an instance of September, (TemporalCompositionFn ThisSeptember Day) denotes the Class of consecutive days that make up ThisSeptember. Note that one can obtain the number of instances of this Class by using the function CardinalityFn.

Ontology

SUMO / TEMPORAL-CONCEPTS

Class(es)

Kategorie

inheritable relation

zeitliche Relation
is instance of

Kategorie

inheritable relation

zweistellige Funktion
is instance of

ZeitlicheAufbauFn

Coordinate term(s)

AdditionFn AnfangFn TagFn DichteFn DivisionFn AusgabeFn EndeFn ExponentiationFn ZukunftFn GraphPfadFn StundeFn SofortigeZukunftFn DirektVergangenheitFn DurchschnittFn AbstandFn KappaFn ListeVerkettenFn ListeOrdnungFn LogarithmusFn MaximumFn MaximalerBelasteterPfadFn MassFn MereologischeDifferenzFn MereologischesProduktFn MereologischeSummeFn MinumumFn MinimalerBelasteterPfadFn MinuteFn MonatFn MultiplikationFn VergangenheitFn PeriodikumAusgabeFn RückläufigeZeitAbstandFn RelativeErgänzungFn RelativeZeitFn RestFn SekundFn ReiheBandeFn GeschwindigkeitFn SubtraktionFn ZeitabstandFn VereinigungFn WennFn WoFn JahrFn vor vorOderGleichzeitig zusammenGeschiecht früh beendet schliesstZeitlichAn decktSichZeitlich zeitlichZwischen zeitlichZwischenOderGleichzeitig zeit

Type restrictions

subclass Zeitabstand TemporalCompositionFn(Zeitabstand, subclass Zeitabstand)

Axioms (13)

wenn "Aufspaltung von interval auf ? interval-types" ist gleich class ,
dann für jeden time1,time2 gilt: wenn time1 ist ein fall von interval-type und time2 ist ein fall von class , dann es gibt ein duration der dauer von time1 ist duration und dauer von time2 ist duration

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1 ?TIME2)
            (=>
                  (and
                        (instance ?TIME1 ?INTERVAL-TYPE)
                        (instance ?TIME2 ?CLASS))
                  (exists
                        (?DURATION)
                        (and
                              (duration ?TIME1 ?DURATION)
                              (duration ?TIME2 ?DURATION))))))

wenn "Aufspaltung von interval auf ? interval-types" ist gleich class ,
dann für jeden time1,time2 gilt: wenn time1 ist ein fall von class und time2 ist ein fall von class und time1 ist gleich time2 nicht, dann time1 schliesst time2 zeitlich an oder time2 schliesst time1 zeitlich an oder time1 geschieht früh als time2 oder time2 geschieht früh als time1

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1 ?TIME2)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (instance ?TIME2 ?CLASS)
                        (not
                              (equal ?TIME1 ?TIME2)))
                  (or
                        (meetsTemporally ?TIME1 ?TIME2)
                        (meetsTemporally ?TIME2 ?TIME1)
                        (earlier ?TIME1 ?TIME2)
                        (earlier ?TIME2 ?TIME1)))))

Wenn "Aufspaltung von interval auf ? interval-types" ist gleich class , dann es gibt ein class time der time beginnt interval .

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (exists
            (?TIME)
            (and
                  (instance ?TIME ?CLASS)
                  (starts ?TIME ?INTERVAL))))

Wenn "Aufspaltung von interval auf ? interval-types" ist gleich class , dann es gibt ein class time der time beendet interval .

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (exists
            (?TIME)
            (and
                  (instance ?TIME ?CLASS)
                  (finishes ?TIME ?INTERVAL))))

wenn "Aufspaltung von interval auf ? interval-types" ist gleich class ,
dann für jeden time1 gilt: wenn time1 ist ein fall von class und time1 beendet interval nicht, dann es gibt ein class time2 der time1 schliesst time2 zeitlich an

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (not
                              (finishes ?TIME1 ?INTERVAL)))
                  (exists
                        (?TIME2)
                        (and
                              (instance ?TIME2 ?CLASS)
                              (meetsTemporally ?TIME1 ?TIME2))))))

wenn "Aufspaltung von interval auf ? interval-types" ist gleich class ,
dann für jeden time1 gilt: wenn time1 ist ein fall von class und time1 beginnt interval nicht, dann es gibt ein class time2 der time2 schliesst time1 zeitlich an

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (not
                              (starts ?TIME1 ?INTERVAL)))
                  (exists
                        (?TIME2)
                        (and
                              (instance ?TIME2 ?CLASS)
                              (meetsTemporally ?TIME2 ?TIME1))))))

wenn "Aufspaltung von interval auf ? interval-types" ist gleich class ,
dann für jeden time gilt: wenn time ist ein fall von Zeitpunkt und time ist ein teil von interval , dann es gibt ein class instance der time ist ein teil von 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))))))

Wenn year ist ein fall von Jahr , dann "die Zahl Fällen in "Aufspaltung von year auf ? Monats"" ist gleich .

(=>
      (instance ?YEAR Year)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?YEAR Month))
            12))

Wenn month ist ein fall von Monat und dauer von month ist "number day duration(s)" , dann "die Zahl Fällen in "Aufspaltung von month auf ? Tags"" ist gleich number .

(=>
      (and
            (instance ?MONTH Month)
            (duration
                  ?MONTH
                  (MeasureFn ?NUMBER DayDuration)))
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MONTH Day))
            ?NUMBER))

Wenn week ist ein fall von Woche , dann "die Zahl Fällen in "Aufspaltung von week auf ? Tags"" ist gleich .

(=>
      (instance ?WEEK Week)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?WEEK Day))
            7))

Wenn day ist ein fall von Tag , dann "die Zahl Fällen in "Aufspaltung von day auf ? Stundes"" ist gleich .

(=>
      (instance ?DAY Day)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?DAY Hour))
            24))

Wenn hour ist ein fall von Stunde , dann "die Zahl Fällen in "Aufspaltung von hour auf ? Minutes"" ist gleich .

(=>
      (instance ?HOUR Hour)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?HOUR Minute))
            60))

Wenn minute ist ein fall von Minute , dann "die Zahl Fällen in "Aufspaltung von minute auf ? Sekundes"" ist gleich .

(=>
      (instance ?MINUTE Minute)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MINUTE Second))
            60))