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
-------------------------


s__documentation(s__TemporalCompositionFn__m,s__ChineseLanguage,'"这是表示以较小的 TimeInterval 组成较大的 TimeInterval 的基本 Function。例如:如果 ThisSeptember 是 September 的一个 instance, 那么(TemporalCompositionFn ThisSeptember Day)表示构成 ThisSeptember 内连续日数的 Class。注:我们可以用函数 CardinalityFn 来得出这个 Class 实例的数目。"')

chinese_format.kif 2819-2822
s__documentation(s__TemporalCompositionFn__m,s__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 9003-9008
s__domain(s__TemporalCompositionFn__m,n__1,s__TimeInterval)

Merge.kif 9000-9000 The number 1 argument of temporal composition is an instance of time interval
s__domainSubclass(s__TemporalCompositionFn__m,n__2,s__TimeInterval)

Merge.kif 9001-9001 The number 2 argument of temporal composition is a subclass of time interval
s__instance(s__TemporalCompositionFn__m,s__BinaryFunction)

s__instance(s__BinaryFunction,s__SetOrClass)

Merge.kif 8998-8998 Temporal composition is an instance of binary function
s__instance(s__TemporalCompositionFn__m,s__TemporalRelation)

s__instance(s__TemporalRelation,s__SetOrClass)

Merge.kif 8997-8997 Temporal composition is an instance of temporal relation
s__instance(s__TotalValuedRelation,s__SetOrClass)

s__instance(s__TemporalCompositionFn__m,s__TotalValuedRelation)

Merge.kif 8999-8999 Temporal composition is an instance of total valued relation
s__rangeSubclass(s__TemporalCompositionFn__m,s__TimeInterval)

Merge.kif 9002-9002 The values returned by temporal composition are subclasses of time interval

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


s__format(s__ChineseLanguage,s__TemporalCompositionFn__m,'"分拆 %1 为 %3 的 %2"')

chinese_format.kif 447-447
s__format(s__EnglishLanguage,s__TemporalCompositionFn__m,'"decomposition of %1 into %3 %2s"')

english_format.kif 456-456
s__termFormat(s__ChineseLanguage,s__TemporalCompositionFn__m,'"时间分拆函数"')

chinese_format.kif 448-448
s__termFormat(s__ChineseLanguage,s__TemporalCompositionFn__m,'"时间构成"')

domainEnglishFormat.kif 57401-57401
s__termFormat(s__ChineseTraditionalLanguage,s__TemporalCompositionFn__m,'"時間構成"')

domainEnglishFormat.kif 57400-57400
s__termFormat(s__EnglishLanguage,s__TemporalCompositionFn__m,'"temporal composition"')

domainEnglishFormat.kif 57399-57399

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


( ! [V__INTERVALTYPE,V__INTERVAL,V__CLASS] :
   (((s__subclass(V__INTERVALTYPE,s__TimeInterval) &
         s__instance(V__INTERVAL,s__TimeInterval) &
         s__subclass(V__CLASS,s__TimeInterval) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__TemporalCompositionFn(V__INTERVAL,V__INTERVALTYPE)
           = V__CLASS)
         =>
         (( ? [V__TIME] :
             ((s__instance(V__TIME,s__TimeInterval) &
                 (s__instance(V__TIME,V__CLASS)
                 &
                 s__finishes(V__TIME,V__INTERVAL)))))))))
)
)

Merge.kif 9043-9048
( ! [V__INTERVALTYPE,V__INTERVAL,V__CLASS] :
   (((s__subclass(V__INTERVALTYPE,s__TimeInterval) &
         s__instance(V__INTERVAL,s__TimeInterval) &
         s__subclass(V__CLASS,s__TimeInterval) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__TemporalCompositionFn(V__INTERVAL,V__INTERVALTYPE)
           = V__CLASS)
         =>
         (( ? [V__TIME] :
             ((s__instance(V__TIME,s__TimeInterval) &
                 (s__instance(V__TIME,V__CLASS)
                 &
                 s__starts(V__TIME,V__INTERVAL)))))))))
)
)

Merge.kif 9036-9041
( ! [V__INTERVALTYPE,V__INTERVAL,V__CLASS] :
   (((s__subclass(V__INTERVALTYPE,s__TimeInterval) &
         s__instance(V__INTERVAL,s__TimeInterval) &
         s__subclass(V__CLASS,s__TimeInterval) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__TemporalCompositionFn(V__INTERVAL,V__INTERVALTYPE)
           = V__CLASS)
         =>
         (( ! [V__TIME] :
             (((s__instance(V__TIME,s__TimePoint) &
                   s__temporalPart(V__TIME,V__INTERVAL))
               =>
               (( ? [V__INSTANCE] :
                   ((s__instance(V__INSTANCE,s__TimePosition) &
                       (s__instance(V__INSTANCE,V__CLASS)
                       &
                       s__temporalPart(V__TIME,V__INSTANCE)))))))))))))
)
)

Merge.kif 9074-9084
( ! [V__INTERVALTYPE,V__INTERVAL,V__CLASS] :
   (((s__subclass(V__INTERVALTYPE,s__TimeInterval) &
         s__instance(V__INTERVAL,s__TimeInterval) &
         s__subclass(V__CLASS,s__TimeInterval) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__TemporalCompositionFn(V__INTERVAL,V__INTERVALTYPE)
           = V__CLASS)
         =>
         (( ! [V__TIME1, V__TIME2] :
             (((s__instance(V__TIME1,s__TimeInterval) &
                   s__instance(V__TIME2,s__TimeInterval))
                 =>
                 (((s__instance(V__TIME1,V__CLASS)
                     &
                     s__instance(V__TIME2,V__CLASS)
                   &
                   ~((V__TIME1 = V__TIME2)))
                 =>
                 ((s__meetsTemporally(V__TIME1,V__TIME2)
                   |
                   s__meetsTemporally(V__TIME2,V__TIME1)
                 |
                 s__earlier(V__TIME1,V__TIME2)
               |
               s__earlier(V__TIME2,V__TIME1))))))))))))
)
)

Merge.kif 9022-9034
( ! [V__INTERVALTYPE,V__INTERVAL,V__CLASS] :
   (((s__subclass(V__INTERVALTYPE,s__TimeInterval) &
         s__instance(V__INTERVALTYPE,s__Class) &
         s__instance(V__INTERVAL,s__TimeInterval) &
         s__subclass(V__CLASS,s__TimeInterval) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__TemporalCompositionFn(V__INTERVAL,V__INTERVALTYPE)
           = V__CLASS)
         =>
         (( ! [V__TIME1, V__TIME2] :
             (((s__instance(V__TIME1,s__TimeInterval) &
                   s__instance(V__TIME2,s__TimeInterval))
                 =>
                 (((s__instance(V__TIME1,V__INTERVALTYPE)
                     &
                     s__instance(V__TIME2,V__CLASS))
                 =>
                 (( ? [V__DURATION] :
                     ((s__instance(V__DURATION,s__TimeDuration) &
                         (s__duration(V__TIME1,V__DURATION)
                         &
                         s__duration(V__TIME2,V__DURATION)))))))))))))))
)
)

Merge.kif 9010-9020
( ! [V__INTERVALTYPE,V__INTERVAL,V__CLASS] :
   (((s__subclass(V__INTERVALTYPE,s__TimeInterval) &
         s__instance(V__INTERVAL,s__TimeInterval) &
         s__subclass(V__CLASS,s__TimeInterval) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__TemporalCompositionFn(V__INTERVAL,V__INTERVALTYPE)
           = V__CLASS)
         =>
         (( ! [V__TIME1] :
             ((s__instance(V__TIME1,s__TimeInterval) =>
                 (((s__instance(V__TIME1,V__CLASS)
                     &
                     ~(s__finishes(V__TIME1,V__INTERVAL)))
                 =>
                 (( ? [V__TIME2] :
                     ((s__instance(V__TIME2,s__TimeInterval) &
                         (s__instance(V__TIME2,V__CLASS)
                         &
                         s__meetsTemporally(V__TIME1,V__TIME2)))))))))))))))
)
)

Merge.kif 9050-9060
( ! [V__INTERVALTYPE,V__INTERVAL,V__CLASS] :
   (((s__subclass(V__INTERVALTYPE,s__TimeInterval) &
         s__instance(V__INTERVAL,s__TimeInterval) &
         s__subclass(V__CLASS,s__TimeInterval) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__TemporalCompositionFn(V__INTERVAL,V__INTERVALTYPE)
           = V__CLASS)
         =>
         (( ! [V__TIME1] :
             ((s__instance(V__TIME1,s__TimeInterval) =>
                 (((s__instance(V__TIME1,V__CLASS)
                     &
                     ~(s__starts(V__TIME1,V__INTERVAL)))
                 =>
                 (( ? [V__TIME2] :
                     ((s__instance(V__TIME2,s__TimeInterval) &
                         (s__instance(V__TIME2,V__CLASS)
                         &
                         s__meetsTemporally(V__TIME2,V__TIME1)))))))))))))))
)
)

Merge.kif 9062-9072

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


( ! [V__MONTH,V__NUMBER] :
   ((s__instance(V__NUMBER,s__Integer) =>
       (((s__instance(V__MONTH,s__Month) &
             s__duration(V__MONTH,s__MeasureFn(V__NUMBER,s__DayDuration)))
         =>
         ((s__CardinalityFn(s__TemporalCompositionFn(V__MONTH,s__Day))
           = V__NUMBER)))))
)
)

Merge.kif 9090-9094
( ! [V__DAY] :
   ((s__instance(V__DAY,s__Day) =>
       ((s__CardinalityFn(s__TemporalCompositionFn(V__DAY,s__Hour))
         = n__24)))
   )
)

Merge.kif 9100-9102
( ! [V__HOUR] :
   ((s__instance(V__HOUR,s__Hour) =>
       ((s__CardinalityFn(s__TemporalCompositionFn(V__HOUR,s__Minute))
         = n__60)))
   )
)

Merge.kif 9104-9106
( ! [V__MINUTE] :
   ((s__instance(V__MINUTE,s__Minute) =>
       ((s__CardinalityFn(s__TemporalCompositionFn(V__MINUTE,s__Second))
         = n__60)))
   )
)

Merge.kif 9108-9110
( ! [V__WEEK] :
   ((s__instance(V__WEEK,s__Week) =>
       ((s__CardinalityFn(s__TemporalCompositionFn(V__WEEK,s__Day))
         = n__7)))
   )
)

Merge.kif 9096-9098
( ! [V__YEAR] :
   ((s__instance(V__YEAR,s__Year) =>
       ((s__CardinalityFn(s__TemporalCompositionFn(V__YEAR,s__Month))
         = n__12)))
   )
)

Merge.kif 9086-9088


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 is open source software produced by Articulate Software and its partners