Browsing Interface : Welcome guest : log in 		[  Home |  Graph |  LogLearn |  Editor |  ]  KB:  Language: 
  Formal Language: 

KB Term:  Term intersection
English Word: 

Sigma KEE - TemporalCompositionFn
TemporalCompositionFn

appearance as argument number 1
-------------------------


(instance TemporalCompositionFn TemporalRelation) Merge.kif 9595-9595 Temporal composition is an instance of temporal relation
(instance TemporalCompositionFn BinaryFunction) Merge.kif 9596-9596 Temporal composition is an instance of binary function
(instance TemporalCompositionFn TotalValuedRelation) Merge.kif 9597-9597 Temporal composition is an instance of total valued relation
(domain TemporalCompositionFn 1 TimeInterval) Merge.kif 9598-9598 The number 1 argument of temporal composition is an instance of timeframe
(domainSubclass TemporalCompositionFn 2 TimeInterval) Merge.kif 9599-9599 The number 2 argument of temporal composition is a subclass of timeframe
(rangeSubclass TemporalCompositionFn TimeInterval) Merge.kif 9600-9600 The values returned by temporal composition are subclasses of timeframe
(documentation TemporalCompositionFn EnglishLanguage "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.") Merge.kif 9601-9606 The values returned by temporal composition are subclasses of timeframe

appearance as argument number 2
-------------------------


(termFormat EnglishLanguage TemporalCompositionFn "temporal composition") domainEnglishFormat.kif 57431-57431
(termFormat ChineseTraditionalLanguage TemporalCompositionFn "時間構成") domainEnglishFormat.kif 57432-57432
(termFormat ChineseLanguage TemporalCompositionFn "时间构成") domainEnglishFormat.kif 57433-57433
(format EnglishLanguage TemporalCompositionFn "decomposition of %1 into %3 %2s") english_format.kif 453-453

antecedent
-------------------------


(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVALTYPE) ?CLASS)
    (forall (?TIME1 ?TIME2)
        (=>
            (and
                (instance ?TIME1 ?INTERVALTYPE)
                (instance ?TIME2 ?CLASS))
            (exists (?DURATION)
                (and
                    (duration ?TIME1 ?DURATION)
                    (duration ?TIME2 ?DURATION))))))		 Merge.kif 9608-9618 If equal decomposition of X into Y and Z, then For all TimeIntervals W and V: there exists T such that duration of W is T and duration of V is T
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVALTYPE) ?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)))))		 Merge.kif 9620-9632 If equal decomposition of X into Y and Z, then For all TimeIntervals W and V: if equal W and V, then At least one of the following holds: (1) W meets V (2) V meets W (3) W happens earlier than V (4) V happens earlier than W
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVALTYPE) ?CLASS)
    (exists (?TIME)
        (and
            (instance ?TIME ?CLASS)
            (starts ?TIME ?INTERVAL))))		 Merge.kif 9634-9639 If equal decomposition of X into Y and Z, then there exists W such that W is an instance of Z and W starts X
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVALTYPE) ?CLASS)
    (exists (?TIME)
        (and
            (instance ?TIME ?CLASS)
            (finishes ?TIME ?INTERVAL))))		 Merge.kif 9641-9646 If equal decomposition of X into Y and Z, then there exists W such that W is an instance of Z and W finishes X
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVALTYPE) ?CLASS)
    (forall (?TIME1)
        (=>
            (and
                (instance ?TIME1 ?CLASS)
                (not
                    (finishes ?TIME1 ?INTERVAL)))
            (exists (?TIME2)
                (and
                    (instance ?TIME2 ?CLASS)
                    (meetsTemporally ?TIME1 ?TIME2))))))		 Merge.kif 9648-9658 If equal decomposition of X into Y and Z, then For all TimeInterval W: if W doesn't finish X, then there exists V such that V is an instance of Z and W meets V
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVALTYPE) ?CLASS)
    (forall (?TIME1)
        (=>
            (and
                (instance ?TIME1 ?CLASS)
                (not
                    (starts ?TIME1 ?INTERVAL)))
            (exists (?TIME2)
                (and
                    (instance ?TIME2 ?CLASS)
                    (meetsTemporally ?TIME2 ?TIME1))))))		 Merge.kif 9660-9670 If equal decomposition of X into Y and Z, then For all TimeInterval W: if W doesn't start X, then there exists V such that V is an instance of Z and V meets W
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVALTYPE) ?CLASS)
    (forall (?TIME)
        (=>
            (and
                (instance ?TIME TimePoint)
                (temporalPart ?TIME ?INTERVAL))
            (exists (?INSTANCE)
                (and
                    (instance ?INSTANCE ?CLASS)
                    (temporalPart ?TIME ?INSTANCE))))))		 Merge.kif 9672-9682 If equal decomposition of X into Y and Z, then For all TimePosition W: if W is an instance of time point and W is a part of X, then there exists V such that V is an instance of Z and W is a part of V

consequent
-------------------------


(=>
    (instance ?YEAR Year)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?YEAR Month)) 12))		 Merge.kif 9684-9686 If X is an instance of year, then equal the number of instances in decomposition of X into months and 12
(=>
    (and
        (instance ?MONTH Month)
        (duration ?MONTH
            (MeasureFn ?NUMBER DayDuration)))
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?MONTH Day)) ?NUMBER))		 Merge.kif 9688-9692 If X is an instance of month and duration of X is Y day duration(s), then equal the number of instances in decomposition of X into days and Y
(=>
    (instance ?WEEK Week)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?WEEK Day)) 7))		 Merge.kif 9694-9696 If X is an instance of week, then equal the number of instances in decomposition of X into days and 7
(=>
    (instance ?DAY Day)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?DAY Hour)) 24))		 Merge.kif 9698-9700 If X is an instance of day, then equal the number of instances in decomposition of X into hours and 24
(=>
    (instance ?HOUR Hour)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?HOUR Minute)) 60))		 Merge.kif 9702-9704 If X is an instance of hour, then equal the number of instances in decomposition of X into minutes and 60
(=>
    (instance ?MINUTE Minute)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?MINUTE Second)) 60))		 Merge.kif 9706-9708 If X is an instance of minute, then equal the number of instances in decomposition of X into seconds and 60


Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)


Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0.0-ac69cf7a (2026-05-13) is open source software produced by Articulate Software and its partners