Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - TemporalCompositionFn
TemporalCompositionFn

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


(documentation TemporalCompositionFn ChineseLanguage "这是表示以较小的 TimeInterval 组成较大的 TimeInterval 的基本 Function。例如:如果 ThisSeptember 是 September 的一个 instance, 那么(TemporalCompositionFn ThisSeptember Day)表示构成 ThisSeptember 内连续日数的 Class。注:我们可以用函数 CardinalityFn 来得出这个 Class 实例的数目。") Merge.kif 9407-9410
(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 9401-9406
(domain TemporalCompositionFn 1 TimeInterval) Merge.kif 9398-9398 The number 1 argument of temporal composition is an instance of time interval
(domainSubclass TemporalCompositionFn 2 TimeInterval) Merge.kif 9399-9399 The number 2 argument of temporal composition is a subclass of time interval
(instance TemporalCompositionFn BinaryFunction) Merge.kif 9396-9396 Temporal composition is an instance of binary function
(instance TemporalCompositionFn TemporalRelation) Merge.kif 9395-9395 Temporal composition is an instance of temporal relation
(instance TemporalCompositionFn TotalValuedRelation) Merge.kif 9397-9397 Temporal composition is an instance of total valued relation
(rangeSubclass TemporalCompositionFn TimeInterval) Merge.kif 9400-9400 The values returned by temporal composition are subclasses of time interval

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


(format ChineseLanguage TemporalCompositionFn "分拆 %1 为 %3 的 %2") chinese_format.kif 447-447
(format EnglishLanguage TemporalCompositionFn "decomposition of %1 into %3 %2s") english_format.kif 271-271
(termFormat ChineseLanguage TemporalCompositionFn "时间分拆函数") chinese_format.kif 448-448 "时间分拆函数" is the printable form of temporal composition in ChineseLanguage
(termFormat EnglishLanguage TemporalCompositionFn "temporal composition") domainEnglishFormat.kif 9996-9996 "temporal composition" is the printable form of temporal composition in english language

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


(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE) ?CLASS)
    (exists (?TIME)
        (and
            (instance ?TIME ?CLASS)
            (finishes ?TIME ?INTERVAL))))
Merge.kif 9445-9450
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE) ?CLASS)
    (exists (?TIME)
        (and
            (instance ?TIME ?CLASS)
            (starts ?TIME ?INTERVAL))))
Merge.kif 9438-9443
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE) ?CLASS)
    (forall (?TIME)
        (=>
            (and
                (instance ?TIME TimePoint)
                (temporalPart ?TIME ?INTERVAL))
            (exists (?INSTANCE)
                (and
                    (instance ?INSTANCE ?CLASS)
                    (temporalPart ?TIME ?INSTANCE))))))
Merge.kif 9476-9486
(=>
    (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)))))
Merge.kif 9424-9436
(=>
    (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))))))
Merge.kif 9412-9422
(=>
    (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))))))
Merge.kif 9452-9462
(=>
    (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))))))
Merge.kif 9464-9474

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


(=>
    (and
        (instance ?MONTH Month)
        (duration ?MONTH
            (MeasureFn ?NUMBER DayDuration)))
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?MONTH Day)) ?NUMBER))
Merge.kif 9492-9496
(=>
    (instance ?DAY Day)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?DAY Hour)) 24))
Merge.kif 9502-9504
(=>
    (instance ?HOUR Hour)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?HOUR Minute)) 60))
Merge.kif 9506-9508
(=>
    (instance ?MINUTE Minute)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?MINUTE Second)) 60))
Merge.kif 9510-9512
(=>
    (instance ?WEEK Week)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?WEEK Day)) 7))
Merge.kif 9498-9500
(=>
    (instance ?YEAR Year)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?YEAR Month)) 12))
Merge.kif 9488-9490


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 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners