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 实例的数目。") chinese_format.kif 2819-2822
(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 8694-8699
(domain TemporalCompositionFn 1 TimeInterval) Merge.kif 8691-8691
(domainSubclass TemporalCompositionFn 2 TimeInterval) Merge.kif 8692-8692
(instance TemporalCompositionFn BinaryFunction) Merge.kif 8689-8689
(instance TemporalCompositionFn TemporalRelation) Merge.kif 8688-8688
(instance TemporalCompositionFn TotalValuedRelation) Merge.kif 8690-8690
(rangeSubclass TemporalCompositionFn TimeInterval) Merge.kif 8693-8693

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 456-456
(termFormat ChineseLanguage TemporalCompositionFn "时间分拆函数") chinese_format.kif 448-448
(termFormat ChineseLanguage TemporalCompositionFn "时间构成") domainEnglishFormat.kif 57373-57373
(termFormat ChineseTraditionalLanguage TemporalCompositionFn "時間構成") domainEnglishFormat.kif 57372-57372
(termFormat EnglishLanguage TemporalCompositionFn "temporal composition") domainEnglishFormat.kif 57371-57371

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


(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE) ?CLASS)
    (exists (?TIME)
        (and
            (instance ?TIME ?CLASS)
            (finishes ?TIME ?INTERVAL))))
Merge.kif 8734-8739
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE) ?CLASS)
    (exists (?TIME)
        (and
            (instance ?TIME ?CLASS)
            (starts ?TIME ?INTERVAL))))
Merge.kif 8727-8732
(=>
    (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 8765-8775
(=>
    (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 8713-8725
(=>
    (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 8701-8711
(=>
    (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 8741-8751
(=>
    (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 8753-8763

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


(=>
    (and
        (instance ?MONTH Month)
        (duration ?MONTH
            (MeasureFn ?NUMBER DayDuration)))
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?MONTH Day)) ?NUMBER))
Merge.kif 8781-8785
(=>
    (instance ?DAY Day)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?DAY Hour)) 24))
Merge.kif 8791-8793
(=>
    (instance ?HOUR Hour)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?HOUR Minute)) 60))
Merge.kif 8795-8797
(=>
    (instance ?MINUTE Minute)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?MINUTE Second)) 60))
Merge.kif 8799-8801
(=>
    (instance ?WEEK Week)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?WEEK Day)) 7))
Merge.kif 8787-8789
(=>
    (instance ?YEAR Year)
    (equal
        (CardinalityFn
            (TemporalCompositionFn ?YEAR Month)) 12))
Merge.kif 8777-8779


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