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

Formal Language: 



KB Term:  Term intersection
English Word: 

  MultiplicationFn

Sigma KEE - MultiplicationFn
MultiplicationFn

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


s__documentation(s__MultiplicationFn__m,s__ChineseLanguage,'如果 ?NUMBER1 和 ?NUMBER2 是 Number,那么 (MultiplicationFn ?NUMBER1 ?NUMBER2)就是这些数字的算术积。')

Merge.kif 4837-4838
s__documentation(s__MultiplicationFn__m,s__EnglishLanguage,'If ?NUMBER1 and ?NUMBER2 are Numbers, then (MultiplicationFn ?NUMBER1 ?NUMBER2) is the arithmetical product of these numbers.')

Merge.kif 4834-4836
s__domain(s__MultiplicationFn__m,1,s__Quantity)

Merge.kif 4831-4831
s__domain(s__MultiplicationFn__m,2,s__Quantity)

Merge.kif 4832-4832
s__identityElement(s__MultiplicationFn__m,1)

Merge.kif 5372-5372
s__instance(s__MultiplicationFn__m,s__AssociativeFunction)

Merge.kif 4827-4827
s__instance(s__BinaryFunction,s__SetOrClass)

Merge.kif 4826-4826
s__instance(s__MultiplicationFn__m,s__CommutativeFunction)

Merge.kif 4828-4828
s__instance(s__TotalValuedRelation,s__SetOrClass)

Merge.kif 4830-4830
s__range(s__MultiplicationFn__m,s__Quantity)

Merge.kif 4833-4833

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


s__format(s__ChineseLanguage,s__MultiplicationFn__m,'%*[*]')

chinese_format.kif 680-680
s__format(s__EnglishLanguage,s__MultiplicationFn__m,'%*[*]')

english_format.kif 424-424
s__format(s__FrenchLanguage,s__MultiplicationFn__m,'%*[*]')

french_format.kif 413-413
s__format(s__ItalianLanguage,s__MultiplicationFn__m,'%*[*]')

relations-it.txt 196-196
s__format(s__PortugueseLanguage,s__MultiplicationFn__m,'%*[*]')

portuguese_format.kif 365-365
s__format(s__cz__m,s__MultiplicationFn__m,'%*[*]')

relations-cz.txt 422-422
s__format(s__de__m,s__MultiplicationFn__m,'%*[*]')

relations-de.txt 887-887
s__format(s__hi__m,s__MultiplicationFn__m,'%*[*]')

relations-hindi.txt 234-234
s__format(s__tg__m,s__MultiplicationFn__m,'%*[*]')

relations-tg.txt 377-377
s__termFormat(s__ChineseLanguage,s__MultiplicationFn__m,'乘法函数')

chinese_format.kif 681-681
s__termFormat(s__EnglishLanguage,s__MultiplicationFn__m,'multiplication')

domainEnglishFormat.kif 6950-6950
s__termFormat(s__tg__m,s__MultiplicationFn__m,'tungkulin ng pagpaparami')

relations-tg.txt 378-378

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


( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__UNIT,V__AMOUNT]
   ((s__arableLandArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))

s__instance(V__UNIT,s__UnitOfArea) ∧
(V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))

s__arableLandArea(V__REGION,V__AMOUNT))
)

Geography.kif 2028-2035
( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__AMOUNT]
   ((s__arableLandArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,V__TOTAL)

s__instance(V__TOTAL,s__AreaMeasure) ∧
(V__AMOUNT = s__MultiplicationFn(V__FRACTION,V__TOTAL)))

s__arableLandArea(V__REGION,V__AMOUNT))
)

Geography.kif 2019-2026
( ∀ [V__N4,V__N1,V__N2,V__N3,V__QUANT]
   (((V__N4 = s__MultiplicationFn(V__N1,s__MultiplicationFn(V__N2,V__N3)))
   ∧
   (V__QUANT = s__MultiplicationFn(s__MeasureFn(V__N1,s__FootLength),s__MultiplicationFn(s__MeasureFn(V__N2,s__FootLength),s__MeasureFn(V__N3,s__FootLength)))))

(V__QUANT = s__MeasureFn(V__N4,s__CubicFoot)))
)

Mid-level-ontology.kif 11231-11241
( ∀ [V__ROBOT,V__INSTANCE,V__OBJECT,V__WIDTHLIMIT,V__LENGTH,V__WIDTH,V__HEIGHT,V__RADIUS]
   ((s__instance(V__ROBOT,s__CarryBot) ∧
       s__instance(V__INSTANCE,V__OBJECT)
     ∧
     s__subclass(V__OBJECT,s__Object) ∧
     s__widthLimit(V__ROBOT,V__WIDTHLIMIT)
   ∧
   ((s__defaultMaximumLength(V__OBJECT,V__LENGTH)
     ∧
     s__defaultMaximumWidth(V__OBJECT,V__WIDTH)
   ∧
   s__defaultMaximumHeight(V__OBJECT,V__HEIGHT)

s__greaterThan(V__LENGTH,V__WIDTHLIMIT)

s__greaterThan(V__WIDTH,V__WIDTHLIMIT)

s__greaterThan(V__HEIGHT,V__WIDTHLIMIT))

(s__defaultMaximumSphereRadius(V__OBJECT,V__RADIUS)

s__greaterThan(s__MultiplicationFn(V__RADIUS,2)
,V__WIDTHLIMIT))))

s__canCarry(V__ROBOT,V__INSTANCE)))
)

Robot.kif 27-45
( ∀ [V__ROBOT,V__LENGTHLIMIT,V__INSTANCE,V__OBJECT,V__LENGTH,V__WIDTH,V__HEIGHT,V__RADIUS]
   ((s__lengthLimit(V__ROBOT,V__LENGTHLIMIT)
     ∧
     s__instance(V__INSTANCE,V__OBJECT)
   ∧
   s__subclass(V__OBJECT,s__Object) ∧
   ((s__defaultMaximumLength(V__OBJECT,V__LENGTH)
     ∧
     s__defaultMaximumWidth(V__OBJECT,V__WIDTH)
   ∧
   s__defaultMaximumHeight(V__OBJECT,V__HEIGHT))

((s__greaterThan(V__LENGTH,V__LENGTHLIMIT)

s__greaterThan(V__WIDTH,V__LENGTHLIMIT))

(s__greaterThan(V__LENGTH,V__LENGTHLIMIT)

s__greaterThan(V__HEIGHT,V__LENGTHLIMIT))

(s__greaterThan(V__WIDTH,V__LENGTHLIMIT)

s__greaterThan(V__HEIGHT,V__LENGTHLIMIT)))

(s__defaultMaximumSphereRadius(V__OBJECT,V__RADIUS)

s__greaterThan(s__MultiplicationFn(V__RADIUS,2)
,s__DivisionFn(V__LENGTHLIMIT,2)))))

s__canCarry(V__ROBOT,V__INSTANCE)))
)

Robot.kif 54-78
( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__UNIT,V__AMOUNT]
   ((s__otherLandUseArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))

s__instance(V__UNIT,s__UnitOfArea) ∧
(V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))

s__otherLandUseArea(V__REGION,V__AMOUNT))
)

Geography.kif 2118-2125
( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__AMOUNT]
   ((s__otherLandUseArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,V__TOTAL)

s__instance(V__TOTAL,s__AreaMeasure) ∧
(V__AMOUNT = s__MultiplicationFn(V__FRACTION,V__TOTAL)))

s__otherLandUseArea(V__REGION,V__AMOUNT))
)

Geography.kif 2109-2116
( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__UNIT,V__AMOUNT]
   ((s__permanentCropLandArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))

s__instance(V__UNIT,s__UnitOfArea) ∧
(V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))

s__permanentCropLandArea(V__REGION,V__AMOUNT))
)

Geography.kif 2076-2083
( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__AMOUNT]
   ((s__permanentCropLandArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,V__TOTAL)

s__instance(V__TOTAL,s__AreaMeasure) ∧
(V__AMOUNT = s__MultiplicationFn(V__FRACTION,V__TOTAL)))

s__permanentCropLandArea(V__REGION,V__AMOUNT))
)

Geography.kif 2067-2074
( ∀ [V__Account,V__Balance,V__Rate,V__Interest,V__Period,V__Rate_Decimal,V__Add,V__Exponent,V__Multiply]
   ((s__principalAmount(V__Account,V__Balance)
     ∧
     s__fixedInterestRate(V__Account,V__Rate)
   ∧
   s__compoundInterest(V__Account,V__Interest,V__Period)

(V__Rate_Decimal = s__DivisionFn(V__Rate,100))

(V__Add = s__AdditionFn(1,V__Rate_Decimal))

(V__Exponent = s__ExponentiationFn(V__Add,s__MagnitudeFn(V__Period)))

(V__Multiply = s__MultiplicationFn(V__Exponent,V__Balance)))

(V__Interest = s__SubtractionFn(V__Multiply,V__Balance)))
)

FinancialOntology.kif 532-541
( ∀ [V__AREA,V__SECTOR,V__FRACTION,V__PERIOD,V__GDPAMOUNT,V__AMOUNT]
   ((s__sectorCompositionOfGDPInPeriod(V__AREA,V__SECTOR,V__FRACTION,V__PERIOD)
     ∧
     s__totalGDPInPeriod(V__AREA,V__GDPAMOUNT,V__PERIOD)
   ∧
   (V__AMOUNT = s__MultiplicationFn(V__FRACTION,V__GDPAMOUNT)))

s__sectorValueOfGDPInPeriod(V__AREA,V__SECTOR,V__AMOUNT,V__PERIOD))
)

Economy.kif 1103-1108
( ∀ [V__Account,V__Interest,V__Period,V__Principal,V__Rate_Decimal,V__Rate]
   ((s__simpleInterest(V__Account,V__Interest,V__Period)
     ∧
     s__principalAmount(V__Account,V__Principal)
   ∧
   (V__Rate_Decimal = s__DivisionFn(V__Interest,V__Principal))

(V__Rate = s__MultiplicationFn(V__Rate_Decimal,100)))

s__interestRatePerPeriod(V__Account,V__Rate,V__Period))
)

FinancialOntology.kif 551-557
( ∀ [V__N]
   ((V__N = s__MultiplicationFn(1,V__N))
   ⇒
   (s__MeasureFn(V__N,s__MillenniumDuration) = s__MeasureFn(s__MultiplicationFn(V__N,1000)
  ,s__YearDuration)))
)

Mid-level-ontology.kif 11266-11270
( ∀ [V__NUM]
   ((V__NUM = s__MultiplicationFn(1,V__NUM))
   ⇒
   (s__MeasureFn(V__NUM,s__NauticalMile) = s__MeasureFn(s__MultiplicationFn(V__NUM,1.151)
  ,s__Mile)))
)

Geography.kif 3706-3708
( ∀ [V__NUM]
   ((V__NUM = s__MultiplicationFn(1,V__NUM))
   ⇒
   (s__MeasureFn(V__NUM,s__NauticalMile) = s__MeasureFn(s__MultiplicationFn(V__NUM,1.852)
  ,s__KiloFn(s__Meter))))
)

Geography.kif 3698-3700
( ∀ [V__NUM]
   ((V__NUM = s__MultiplicationFn(1,V__NUM))
   ⇒
   (s__MeasureFn(V__NUM,s__NauticalMile) = s__MeasureFn(s__MultiplicationFn(V__NUM,1852)
  ,s__Meter)))
)

Geography.kif 3694-3696
( ∀ [V__NUM]
   ((V__NUM = s__MultiplicationFn(1,V__NUM))
   ⇒
   (s__MeasureFn(V__NUM,s__NauticalMile) = s__MeasureFn(s__MultiplicationFn(V__NUM,6076.1)
  ,s__FootLength)))
)

Geography.kif 3702-3704
( ∀ [V__NUM]
   ((V__NUM = s__MultiplicationFn(1,V__NUM))
   ⇒
   (s__MeasureFn(V__NUM,s__SquareKilometer) = s__MeasureFn(s__MultiplicationFn(V__NUM,1000000)
  ,s__SquareMeter)))
)

Geography.kif 624-627
( ∀ [V__NUMBER]
   ((V__NUMBER = s__MultiplicationFn(1,V__NUMBER))
   ⇒
   (s__MeasureFn(V__NUMBER,s__CenturyDuration) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,100)
  ,s__YearDuration)))
)

Mid-level-ontology.kif 16733-16737
( ∀ [V__NUMBER]
   ((V__NUMBER = s__MultiplicationFn(1,V__NUMBER))
   ⇒
   (s__MeasureFn(V__NUMBER,s__DecadeDuration) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,10)
  ,s__YearDuration)))
)

Mid-level-ontology.kif 16742-16746
( ∀ [V__NUMBER]
   ((V__NUMBER = s__MultiplicationFn(1,V__NUMBER))
   ⇒
   (s__MeasureFn(V__NUMBER,s__Fathom) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,6)
  ,s__FootLength)))
)

Geography.kif 3666-3670
( ∀ [V__NUMBER]
   ((V__NUMBER = s__MultiplicationFn(1,V__NUMBER))
   ⇒
   (s__MeasureFn(V__NUMBER,s__LongTon) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,2240)
  ,s__PoundMass)))
)

Mid-level-ontology.kif 11212-11216
( ∀ [V__NUMBER]
   ((V__NUMBER = s__MultiplicationFn(1,V__NUMBER))
   ⇒
   (s__MeasureFn(V__NUMBER,s__Nanometer) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,0.000000001)
  ,s__Meter)))
)

Mid-level-ontology.kif 16759-16765
( ∀ [V__NUMBER]
   ((V__NUMBER = s__MultiplicationFn(1,V__NUMBER))
   ⇒
   (s__MeasureFn(V__NUMBER,s__RegistryTon) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,100)
  ,s__CubicFoot)))
)

Mid-level-ontology.kif 11251-11255
( ∀ [V__NUMBER]
   ((V__NUMBER = s__MultiplicationFn(1,V__NUMBER))
   ⇒
   (s__MeasureFn(V__NUMBER,s__TonMass) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,2000)
  ,s__PoundMass)))
)

Mid-level-ontology.kif 11185-11189

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


( ∀ [V__UNIT,V__AMOUNT]
   ((s__instance(V__UNIT,s__UnitOfMeasure) ∧
       (V__AMOUNT = s__MeasureFn(1,s__SquareUnitFn(V__UNIT))))
<⇒
(V__AMOUNT = s__MultiplicationFn(s__MeasureFn(1,V__UNIT)
,s__MeasureFn(1,V__UNIT))))
)

Geography.kif 3748-3752
( ∀ [V__NUMBER1,V__NUMBER2,V__NUMBER]
   ((s__RemainderFn(V__NUMBER1,V__NUMBER2)
     = V__NUMBER)
   <⇒
   (s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1))
)

Merge.kif 5248-5250
( ∀ [V__O,V__A]
   (s__measure(V__O,s__MeasureFn(V__A,s__MetricTon))
   <⇒
   s__measure(V__O,s__MeasureFn(s__MultiplicationFn(V__A,2205)
,s__PoundMass)))
)

Mid-level-ontology.kif 11199-11205
( ∀ [V__OBJ,V__DEG]
   (s__measure(V__OBJ,s__MeasureFn(V__DEG,s__AngularDegree))
   <⇒
   s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(60,V__DEG)
,s__ArcMinute)))
)

Geography.kif 378-380
( ∀ [V__OBJ,V__DEG]
   (s__measure(V__OBJ,s__MeasureFn(V__DEG,s__ArcMinute))
   <⇒
   s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(60,V__DEG)
,s__ArcSecond)))
)

Geography.kif 397-399
( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__UNIT]
   ((s__arableLandArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))

s__instance(V__UNIT,s__UnitOfArea))

(∃ [V__ARABLE]
(s__instance(V__ARABLE,s__ArableLand) ∧
s__geographicSubregion(V__ARABLE,V__REGION)

s__measure(V__ARABLE,s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))))
)

Geography.kif 2037-2047
No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 193-210
No TPTP formula. May not be expressible in strict first order. Geography.kif 655-661
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11160-11169
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11171-11180
( ∀ [V__NUMBER]
   ((s__instance(V__NUMBER,s__Integer) ∧
       (¬ (V__NUMBER = 0)))
     ⇒
     (1 = s__MultiplicationFn(V__NUMBER,s__ReciprocalFn(V__NUMBER))))
)

Merge.kif 5229-5234
No TPTP formula. May not be expressible in strict first order. Cars.kif 3066-3080
( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__UNIT]
   ((s__otherLandUseArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))

s__instance(V__UNIT,s__UnitOfArea))

(∃ [V__OTHER]
(s__instance(V__OTHER,s__LandArea) ∧
s__instance(V__OTHER,s__ArableLand))

s__instance(V__OTHER,s__PermanentCropLand))

s__geographicSubregion(V__OTHER,V__REGION)

s__measure(V__OTHER,s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))))
)

Geography.kif 2127-2139
( ∀ [V__REGION,V__FRACTION,V__TOTAL,V__UNIT]
   ((s__permanentCropLandArea(V__REGION,V__FRACTION)
     ∧
     s__greaterThanOrEqualTo(V__FRACTION,0)
   ∧
   s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))

s__instance(V__UNIT,s__UnitOfArea))

(∃ [V__PERMCROP]
(s__instance(V__PERMCROP,s__PermanentCropLand) ∧
s__geographicSubregion(V__PERMCROP,V__REGION)

s__measure(V__PERMCROP,s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))))
)

Geography.kif 2085-2095
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 2161-2171
( ∀ [V__Stocks,V__Number,V__Time,V__N1,V__N2,V__TimeOfSplit,V__N3,V__NewNumber,V__TimeAfterSplit]
   ((s__price(V__Stocks,s__MeasureFn(V__Number,s__UnitedStatesDollar),V__Time)
     ∧
     (∃ [V__Event]
       (s__splitFor(V__Event,V__N1,V__N2)
       ∧
       (s__WhenFn(V__Event)
       = V__TimeOfSplit))))

((V__N3 = s__MultiplicationFn(V__Number,V__N1))

(V__NewNumber = s__DivisionFn(V__N3,V__N2))

s__price(V__Stocks,s__MeasureFn(V__NewNumber,s__UnitedStatesDollar),V__TimeAfterSplit)

s__meetsTemporally(V__Time,V__TimeOfSplit)

s__meetsTemporally(V__TimeOfSplit,V__TimeAfterSplit)))
)

FinancialOntology.kif 2173-2185
( ∀ [V__Account,V__Balance,V__Rate,V__Amount,V__Period,V__Rate_Decimal]
   ((s__principalAmount(V__Account,V__Balance)
     ∧
     s__fixedInterestRate(V__Account,V__Rate)
   ∧
   s__simpleInterest(V__Account,V__Amount,V__Period)

(V__Rate_Decimal = s__DivisionFn(s__MagnitudeFn(V__Rate)
,100)))

(V__Amount = s__MultiplicationFn(s__MultiplicationFn(s__MagnitudeFn(V__Period)
,V__Balance)
,V__Rate_Decimal)))
)

FinancialOntology.kif 514-520
( ∀ [V__F,V__S1,V__S2,V__HF,V__U,V__H1,V__H2]
   (s__attribute(V__F,s__Flat) ⇒
     (s__side(V__S1,V__F)
     ∧
     s__side(V__S2,V__F)
   ∧
   s__meetsSpatially(V__S1,V__S2)

(¬ (V__S1 = V__S2))

s__height(V__F,s__MeasureFn(V__HF,V__U))

s__height(V__S1,s__MeasureFn(V__H1,V__U))

s__height(V__S2,s__MeasureFn(V__H2,V__U))

s__greaterThan(V__H1,s__MultiplicationFn(2,V__HF))

s__greaterThan(V__H2,s__MultiplicationFn(2,V__HF))))
)

Mid-level-ontology.kif 3252-3263
( ∀ [V__F,V__S1,V__S2,V__HF,V__U,V__H1,V__H2]
   (s__attribute(V__F,s__LongAndThin) ⇒
     (s__side(V__S1,V__F)
     ∧
     s__side(V__S2,V__F)
   ∧
   s__meetsSpatially(V__S1,V__S2)

(¬ (V__S1 = V__S2))

s__length(V__F,s__MeasureFn(V__HF,V__U))

s__length(V__S1,s__MeasureFn(V__H1,V__U))

s__length(V__S2,s__MeasureFn(V__H2,V__U))

s__lessThan(V__H1,s__MultiplicationFn(3,V__HF))

s__lessThan(V__H2,s__MultiplicationFn(3,V__HF))))
)

Mid-level-ontology.kif 3276-3287
( ∀ [V__CIRCLE,V__LENGTH]
   (s__diameter(V__CIRCLE,V__LENGTH)
   ⇒
   (∃ [V__N__HALF,V__U__HALF]
     (s__radius(V__CIRCLE,s__MeasureFn(V__N__HALF,V__U__HALF))
   ∧
   (s__MeasureFn(s__MultiplicationFn(V__N__HALF,2)
  ,V__U__HALF)
= V__LENGTH))))
)

Merge.kif 7855-7860
( ∀ [V__C,V__L,V__U]
   ((s__DiameterFn(V__C)
     = s__MeasureFn(V__L,V__U))

(∃ [V__R]
   ((s__RadiusFn(V__C)
     = s__MeasureFn(V__R,V__U))

(s__MultiplicationFn(V__R,2)
= V__L))))
)

Mid-level-ontology.kif 5254-5259
( ∀ [V__NUMBER1,V__NUMBER2]
   ((s__SquareRootFn(V__NUMBER1)
     = V__NUMBER2)
   ⇒
   (s__MultiplicationFn(V__NUMBER2,V__NUMBER2)
   = V__NUMBER1))
)

Merge.kif 5334-5336
( ∀ [V__AMOUNT,V__NUM]
   ((V__AMOUNT = s__MeasureFn(V__NUM,s__NauticalMile))
     ⇒
     (V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__NUM,1.151)
    ,s__Mile)))
)

Geography.kif 3690-3692
( ∀ [V__AMOUNT,V__NUM]
   ((V__AMOUNT = s__MeasureFn(V__NUM,s__NauticalMile))
     ⇒
     (V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__NUM,1.852)
    ,s__KiloFn(s__Meter))))
)

Geography.kif 3686-3688
( ∀ [V__AMOUNT,V__X]
   ((V__AMOUNT = s__MeasureFn(V__X,s__Joule))
     ⇒
     (V__AMOUNT = s__MeasureFn(s__MultiplicationFn(0.0002778,V__X)
    ,s__Watt)))
)

Economy.kif 2020-2022

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement
-------------------------


(s__MeasureFn(1,s__CubicFoot) = s__MultiplicationFn(s__MeasureFn(1,s__FootLength),s__MultiplicationFn(s__MeasureFn(1,s__FootLength),s__MeasureFn(1,s__FootLength))))

Mid-level-ontology.kif 11223-11229
(s__MeasureFn(1,s__SquareKilometer) = s__MultiplicationFn(s__MeasureFn(1,s__KiloFn(s__Meter))
,s__MeasureFn(1,s__KiloFn(s__Meter))))

Geography.kif 621-622
(s__MeasureFn(1,s__SquareMeter) = s__MultiplicationFn(s__MeasureFn(1,s__Meter),s__MeasureFn(1,s__Meter)))

Geography.kif 3736-3737
( ∀ [V__DEG]
   (s__MeasureFn(V__DEG,s__ArcMinute) = s__MeasureFn(s__MultiplicationFn(60,V__DEG)
  ,s__ArcSecond))
)

Geography.kif 402-402
( ∀ [V__MUMBER,V__NUMBER]
   (s__MeasureFn(V__MUMBER,s__Micrometer) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,0.0000001)
  ,s__Meter))
)

Geography.kif 6450-6453
( ∀ [V__NUM]
   (s__MeasureFn(V__NUM,s__AngularDegree) = s__MeasureFn(s__MultiplicationFn(60,V__NUM)
  ,s__ArcMinute))
)

Geography.kif 383-383
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Amu) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1.6605402E-24)
  ,s__Gram))
)

Merge.kif 7404-7406
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Angstrom) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1.0E-10)
  ,s__Meter))
)

Merge.kif 7428-7430
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__AngularDegree) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,s__DivisionFn(s__Pi,180.0))
,s__Radian))
)

Merge.kif 7634-7636
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__BritishThermalUnit) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1055.05585262)
  ,s__Joule))
)

Merge.kif 7620-7622
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Byte) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,8)
  ,s__Bit))
)

Merge.kif 7697-7699
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Calorie) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,4.1868)
  ,s__Joule))
)

Merge.kif 7612-7614
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Centimeter) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,0.01)
  ,s__Meter))
)

Merge.kif 6996-6998
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__DayDuration) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,24)
  ,s__HourDuration))
)

Merge.kif 7343-7345
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__ElectronVolt) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1.60217733E-19)
  ,s__Joule))
)

Merge.kif 7415-7417
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__EuroCent) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,0.01)
  ,s__EuroDollar))
)

Merge.kif 7675-7677
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__FootLength) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,0.3048)
  ,s__Meter))
)

Merge.kif 7441-7443
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__HourDuration) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,60)
  ,s__MinuteDuration))
)

Merge.kif 7351-7353
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Inch) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,0.0254)
  ,s__Meter))
)

Merge.kif 7449-7451
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__KiloByte) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1024)
  ,s__Byte))
)

Merge.kif 7708-7710
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Kilogram) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1000)
  ,s__Gram))
)

Merge.kif 7541-7544
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Kilometer) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1000)
  ,s__Meter))
)

Merge.kif 7016-7019
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__MegaByte) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1024)
  ,s__KiloByte))
)

Merge.kif 7719-7721
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Mile) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1609.344)
  ,s__Meter))
)

Merge.kif 7457-7459
( ∀ [V__NUMBER]
   (s__MeasureFn(V__NUMBER,s__Millimeter) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,0.001)
  ,s__Meter))
)

Merge.kif 7005-7008

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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

Show without tree


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