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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - SpeedFn
SpeedFn

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


s__documentation(s__SpeedFn__m,s__ChineseLanguage,'"这个函数把LengthMeasure 的一个实例和 TimeDuration 的一个实例和由这个时间和距离比例所代表的速率联系起来。例如: (SpeedFn (MeasureFn 55 Mile)(MeasureFn 1 HourDuration))表示速度55英里每小时。"')

chinese_format.kif 2483-2485
s__documentation(s__SpeedFn__m,s__EnglishLanguage,'"Maps an instance of LengthMeasure and an instance of TimeDuration to the speed represented by this proportion of distance and time. For example, (SpeedFn (MeasureFn 55 Mile)(MeasureFn 1 HourDuration)) represents the velocity of 55 miles per hour."')

Merge.kif 6451-6454
s__domain(s__SpeedFn__m,n__1,s__LengthMeasure)

Merge.kif 6447-6447 The number 1 argument of speed is an instance of length measure
s__domain(s__SpeedFn__m,n__2,s__TimeDuration)

Merge.kif 6448-6448 The number 2 argument of speed is an instance of time duration
s__instance(s__BinaryFunction,s__SetOrClass)

s__instance(s__SpeedFn__m,s__BinaryFunction)

Merge.kif 6446-6446 Speed is an instance of binary function
s__instance(s__SpeedFn__m,s__TotalValuedRelation)

s__instance(s__TotalValuedRelation,s__SetOrClass)

Merge.kif 6445-6445 Speed is an instance of total valued relation
s__range(s__SpeedFn__m,s__FunctionQuantity)

Merge.kif 6449-6449 The range of speed is an instance of function quantity
s__subrelation(s__SpeedFn__m,s__PerFn__m)

Merge.kif 6444-6444 Speed is a subrelation of per

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


s__format(s__ChineseLanguage,s__SpeedFn__m,'"%1 除以 %2"')

chinese_format.kif 659-659
s__format(s__EnglishLanguage,s__SpeedFn__m,'"%1 per %2"')

english_format.kif 665-665
s__termFormat(s__ChineseLanguage,s__SpeedFn__m,'"速度"')

domainEnglishFormat.kif 54585-54585
s__termFormat(s__ChineseLanguage,s__SpeedFn__m,'"速率函数"')

chinese_format.kif 660-660
s__termFormat(s__ChineseTraditionalLanguage,s__SpeedFn__m,'"速度"')

domainEnglishFormat.kif 54584-54584
s__termFormat(s__EnglishLanguage,s__SpeedFn__m,'"speed"')

domainEnglishFormat.kif 54583-54583

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


No TPTP formula. May not be expressible in strict first order. Cars.kif 2884-2902
No TPTP formula. May not be expressible in strict first order. Merge.kif 10715-10723
( ! [V__DIST,V__TIME,V__PLACE,V__ZEPHYR,V__X] :
   (((s__instance(V__DIST,s__LengthMeasure) &
         s__instance(V__TIME,s__TimeDuration) &
         s__instance(V__X,s__RealNumber))
       =>
       (((s__instance(V__ZEPHYR,s__WindFlow) &
             s__instance(V__PLACE,s__Object) &
             s__partlyLocated(V__ZEPHYR,V__PLACE)
           &
           s__elevation(V__ZEPHYR,s__MeasureFn(V__X,s__FootLength))
         &
         s__lessThanOrEqualTo(V__X,n__500)
       &
       s__measure(V__ZEPHYR,s__SpeedFn(V__DIST,V__TIME)))
=>
(s__surfaceWindSpeed(V__PLACE,s__SpeedFn(V__DIST,V__TIME))))))
)
)

Weather.kif 148-157
( ! [V__TIME,V__FLUID,V__LENGTH,V__PART] :
   (((s__instance(V__TIME,s__TimeDuration) &
         s__instance(V__FLUID,s__Substance) &
         s__instance(V__FLUID,s__FlowRegion) &
         s__instance(V__LENGTH,s__LengthMeasure) &
         s__instance(V__PART,s__Substance))
       =>
       (((s__measure(s__FlowFn(V__FLUID)
          ,s__SpeedFn(V__LENGTH,V__TIME))
       &
       s__piece(V__PART,V__FLUID))
   =>
   (s__piece(V__PART,s__SpeedFn(V__LENGTH,V__TIME))))))
)
)

Geography.kif 4685-4689
( ! [V__DIST,V__TIME,V__PLACE,V__DIRECTION] :
   (((s__instance(V__DIST,s__LengthMeasure) &
         s__instance(V__TIME,s__TimeDuration) &
         s__instance(V__DIRECTION,s__DirectionalAttribute))
       =>
       (((s__surfaceWindVelocity(V__PLACE,s__SpeedFn(V__DIST,V__TIME)
          ,V__DIRECTION)
         &
         s__instance(V__PLACE,s__WindFlow))
       =>
       (( ? [V__BLOW] :
           ((s__instance(V__BLOW,s__Wind) &
               s__eventPartlyLocated(V__BLOW,V__PLACE)
             &
             s__measure(V__BLOW,s__VelocityFn(V__DIST,V__TIME,V__PLACE,V__DIRECTION)))))))))
)
)

Weather.kif 115-123
No TPTP formula. May not be expressible in strict first order. Transportation.kif 1726-1744
( ! [V__SPEED,V__TIME,V__DISTANCE] :
   (((s__instance(V__SPEED,s__FunctionQuantity) &
         s__instance(V__TIME,s__RealNumber) &
         s__instance(V__DISTANCE,s__RealNumber))
       =>
       (((V__SPEED = s__SpeedFn(s__MeasureFn(V__DISTANCE,s__NauticalMile),s__MeasureFn(V__TIME,s__HourDuration)))
         =>
         ((V__SPEED = s__MeasureFn(s__DivisionFn(V__DISTANCE,V__TIME)
          ,s__KnotUnitOfSpeed))))))
)
)

Geography.kif 3774-3776

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


( ! [V__SPEED,V__NUM] :
   (((s__instance(V__SPEED,s__FunctionQuantity) &
         s__instance(V__NUM,s__RealNumber))
       =>
       ((((V__SPEED = s__MeasureFn(V__NUM,s__MilesPerHour))
             =>
             (V__SPEED = s__SpeedFn(s__MeasureFn(V__NUM,s__Mile),s__MeasureFn(n__1,s__HourDuration))))
         &
         ((V__SPEED = s__SpeedFn(s__MeasureFn(V__NUM,s__Mile),s__MeasureFn(n__1,s__HourDuration)))
         =>
         (V__SPEED = s__MeasureFn(V__NUM,s__MilesPerHour))))))
)
)

Weather.kif 1701-1707 A function quantity is equal to a real number miles per hour(s) if and only if the function quantity is equal to the real number mile(s) per 1 hour duration(s)
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16243-16264
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16271-16291
( ! [V__DIST,V__TIME,V__PLACE,V__BLOW,V__DIRECTION] :
   (((s__instance(V__DIST,s__LengthMeasure) &
         s__instance(V__TIME,s__TimeDuration) &
         s__instance(V__DIRECTION,s__DirectionalAttribute))
       =>
       (((s__instance(V__PLACE,s__Object) &
             s__instance(V__BLOW,s__Wind) &
             s__measure(V__BLOW,s__VelocityFn(V__DIST,V__TIME,V__PLACE,V__DIRECTION)))
       =>
       (s__surfaceWindVelocity(V__PLACE,s__SpeedFn(V__DIST,V__TIME)
      ,V__DIRECTION)))))
)
)

Weather.kif 125-130
( ! [V__DIST,V__TIME,V__PLACE,V__ZEPHYR,V__X] :
   (((s__instance(V__DIST,s__LengthMeasure) &
         s__instance(V__TIME,s__TimeDuration) &
         s__instance(V__X,s__RealNumber))
       =>
       (((s__instance(V__ZEPHYR,s__WindFlow) &
             s__instance(V__PLACE,s__Object) &
             s__partlyLocated(V__ZEPHYR,V__PLACE)
           &
           s__elevation(V__ZEPHYR,s__MeasureFn(V__X,s__FootLength))
         &
         s__lessThanOrEqualTo(V__X,n__500)
       &
       s__measure(V__ZEPHYR,s__SpeedFn(V__DIST,V__TIME)))
=>
(s__surfaceWindSpeed(V__PLACE,s__SpeedFn(V__DIST,V__TIME))))))
)
)

Weather.kif 148-157
( ! [V__TIME,V__FLUID,V__LENGTH,V__PART] :
   (((s__instance(V__TIME,s__TimeDuration) &
         s__instance(V__FLUID,s__Substance) &
         s__instance(V__FLUID,s__FlowRegion) &
         s__instance(V__LENGTH,s__LengthMeasure) &
         s__instance(V__PART,s__Substance))
       =>
       (((s__measure(s__FlowFn(V__FLUID)
          ,s__SpeedFn(V__LENGTH,V__TIME))
       &
       s__piece(V__PART,V__FLUID))
   =>
   (s__piece(V__PART,s__SpeedFn(V__LENGTH,V__TIME))))))
)
)

Geography.kif 4685-4689
( ! [V__SPEED,V__NUM] :
   (((s__instance(V__SPEED,s__FunctionQuantity) &
         s__instance(V__NUM,s__RealNumber))
       =>
       (((V__SPEED = s__MeasureFn(V__NUM,s__KnotUnitOfSpeed))
           =>
           ((V__SPEED = s__SpeedFn(s__MeasureFn(V__NUM,s__NauticalMile),s__MeasureFn(n__1,s__HourDuration)))))))
   )
)

Geography.kif 3778-3780
( ! [V__OBJECT,V__TIME,V__REF,V__DISTANCE,V__DIRECTION] :
   (((s__instance(V__OBJECT,s__Physical) &
         s__instance(V__TIME,s__TimeDuration) &
         s__instance(V__REF,s__Region) &
         s__instance(V__DISTANCE,s__LengthMeasure) &
         s__instance(V__DIRECTION,s__DirectionalAttribute))
       =>
       ((s__measure(V__OBJECT,s__VelocityFn(V__DISTANCE,V__TIME,V__REF,V__DIRECTION))
       =>
       (s__measure(V__OBJECT,s__SpeedFn(V__DISTANCE,V__TIME))))))
)
)

Merge.kif 6469-6471


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