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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - MultiplicationFn
MultiplicationFn

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


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

chinese_format.kif 2212-2213
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 4563-4565
s__domain(s__MultiplicationFn__m,n__1,s__Number)

Merge.kif 4559-4559 The number 1 argument of multiplication is an instance of number
s__domain(s__MultiplicationFn__m,n__2,s__Number)

Merge.kif 4560-4560 The number 2 argument of multiplication is an instance of number
s__identityElement(s__MultiplicationFn__m,n__1)

Merge.kif 5094-5094 1 is an identity element of multiplication
s__instance(s__AssociativeFunction,s__SetOrClass)

s__instance(s__MultiplicationFn__m,s__AssociativeFunction)

Merge.kif 4555-4555 Multiplication is an instance of associative function
s__instance(s__BinaryFunction,s__SetOrClass)

s__instance(s__MultiplicationFn__m,s__BinaryFunction)

Merge.kif 4554-4554 Multiplication is an instance of binary function
s__instance(s__MultiplicationFn__m,s__CommutativeFunction)

s__instance(s__CommutativeFunction,s__SetOrClass)

Merge.kif 4556-4556 Multiplication is an instance of commutative function
s__instance(s__TotalValuedRelation,s__SetOrClass)

s__instance(s__MultiplicationFn__m,s__TotalValuedRelation)

Merge.kif 4558-4558 Multiplication is an instance of total valued relation
s__range(s__MultiplicationFn__m,s__Number)

Merge.kif 4561-4561 The range of multiplication is an instance of number

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 685-685
s__termFormat(s__ChineseLanguage,s__MultiplicationFn__m,'"乘法"')

domainEnglishFormat.kif 39168-39168
s__termFormat(s__ChineseLanguage,s__MultiplicationFn__m,'"乘法函数"')

chinese_format.kif 681-681
s__termFormat(s__ChineseTraditionalLanguage,s__MultiplicationFn__m,'"乘法"')

domainEnglishFormat.kif 39167-39167
s__termFormat(s__EnglishLanguage,s__MultiplicationFn__m,'"multiplication"')

domainEnglishFormat.kif 39166-39166

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


( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__arableLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__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 2061-2068
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__Number) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__arableLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__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 2052-2059
( ! [V__N1,V__N2,V__N3,V__N4,V__QUANT] :
   (((s__instance(V__N1,s__RealNumber) &
         s__instance(V__N2,s__RealNumber) &
         s__instance(V__N3,s__RealNumber) &
         s__instance(V__N4,s__RealNumber) &
         s__instance(V__QUANT,s__Number) &
         s__instance(V__QUANT,s__PhysicalQuantity))
       =>
       ((((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 12839-12849
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__otherLandUseArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__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 2151-2158
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__Number) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__otherLandUseArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__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 2142-2149
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__permanentCropLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__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 2109-2116
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__Number) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__permanentCropLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__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 2100-2107
( ! [V__Period,V__Rate,V__Balance,V__Account,V__Interest,V__Multiply,V__Exponent,V__Rate_Decimal,V__Add] :
   (((s__instance(V__Period,s__TimeInterval) &
         s__instance(V__Rate,s__Number) &
         s__instance(V__Balance,s__Number) &
         s__instance(V__Balance,s__CurrencyMeasure) &
         s__instance(V__Account,s__FinancialAccount) &
         s__instance(V__Interest,s__Interest) &
         s__instance(V__Interest,s__Number) &
         s__instance(V__Multiply,s__Number) &
         s__instance(V__Exponent,s__RealNumber) &
         s__instance(V__Rate_Decimal,s__Number) &
         s__instance(V__Add,s__RealNumber))
       =>
       (((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,n__100))
     &
     (V__Add = s__AdditionFn(n__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__GDPAMOUNT,V__AMOUNT,V__SECTOR,V__AREA,V__FRACTION,V__PERIOD] :
   (((s__instance(V__GDPAMOUNT,s__Number) &
         s__instance(V__GDPAMOUNT,s__CurrencyMeasure) &
         s__instance(V__AMOUNT,s__Number) &
         s__instance(V__AMOUNT,s__CurrencyMeasure) &
         s__instance(V__SECTOR,s__IndustryAttribute) &
         s__instance(V__AREA,s__GeopoliticalArea) &
         s__instance(V__FRACTION,s__RealNumber) &
         s__subclass(V__PERIOD,s__TimeInterval))
       =>
       (((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__Period,V__Rate,V__Account,V__Interest,V__Principal,V__Rate_Decimal] :
   (((s__instance(V__Period,s__TimeInterval) &
         s__instance(V__Rate,s__Number) &
         s__instance(V__Account,s__FinancialAccount) &
         s__instance(V__Interest,s__Interest) &
         s__instance(V__Interest,s__Number) &
         s__instance(V__Principal,s__Number) &
         s__instance(V__Principal,s__CurrencyMeasure) &
         s__instance(V__Rate_Decimal,s__Number))
       =>
       (((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,n__100)))
   =>
   (s__interestRatePerPeriod(V__Account,V__Rate,V__Period)))))
)
)

FinancialOntology.kif 551-557
( ! [V__N] :
   ((s__instance(V__N,s__RealNumber) =>
       (((V__N = s__MultiplicationFn(n__1,V__N))
         =>
         ((s__MeasureFn(V__N,s__MillenniumDuration) = s__MeasureFn(s__MultiplicationFn(V__N,n__1000)
          ,s__YearDuration))))))
)
)

Mid-level-ontology.kif 12874-12878
( ! [V__NUM] :
   ((s__instance(V__NUM,s__RealNumber) =>
       (((V__NUM = s__MultiplicationFn(n__1,V__NUM))
         =>
         ((s__MeasureFn(V__NUM,s__NauticalMile) = s__MeasureFn(s__MultiplicationFn(V__NUM,n__1_151)
          ,s__Mile))))))
)
)

Geography.kif 3762-3764
( ! [V__NUM] :
   ((s__instance(V__NUM,s__RealNumber) =>
       (((V__NUM = s__MultiplicationFn(n__1,V__NUM))
         =>
         ((s__MeasureFn(V__NUM,s__NauticalMile) = s__MeasureFn(s__MultiplicationFn(V__NUM,n__1_852)
          ,s__KiloFn(s__Meter)))))))
)
)

Geography.kif 3754-3756
( ! [V__NUM] :
   ((s__instance(V__NUM,s__RealNumber) =>
       (((V__NUM = s__MultiplicationFn(n__1,V__NUM))
         =>
         ((s__MeasureFn(V__NUM,s__NauticalMile) = s__MeasureFn(s__MultiplicationFn(V__NUM,n__1852)
          ,s__Meter))))))
)
)

Geography.kif 3750-3752
( ! [V__NUM] :
   ((s__instance(V__NUM,s__RealNumber) =>
       (((V__NUM = s__MultiplicationFn(n__1,V__NUM))
         =>
         ((s__MeasureFn(V__NUM,s__NauticalMile) = s__MeasureFn(s__MultiplicationFn(V__NUM,n__6076_1)
          ,s__FootLength))))))
)
)

Geography.kif 3758-3760
( ! [V__NUM] :
   ((s__instance(V__NUM,s__RealNumber) =>
       (((V__NUM = s__MultiplicationFn(n__1,V__NUM))
         =>
         ((s__MeasureFn(V__NUM,s__SquareKilometer) = s__MeasureFn(s__MultiplicationFn(V__NUM,n__1000000)
          ,s__SquareMeter))))))
)
)

Geography.kif 627-630
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       (((V__NUMBER = s__MultiplicationFn(n__1,V__NUMBER))
         =>
         ((s__MeasureFn(V__NUMBER,s__CenturyDuration) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__100)
          ,s__YearDuration))))))
)
)

Mid-level-ontology.kif 18096-18100
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       (((V__NUMBER = s__MultiplicationFn(n__1,V__NUMBER))
         =>
         ((s__MeasureFn(V__NUMBER,s__DecadeDuration) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__10)
          ,s__YearDuration))))))
)
)

Merge.kif 8402-8406
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       (((V__NUMBER = s__MultiplicationFn(n__1,V__NUMBER))
         =>
         ((s__MeasureFn(V__NUMBER,s__Fathom) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__6)
          ,s__FootLength))))))
)
)

Geography.kif 3722-3726
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       (((V__NUMBER = s__MultiplicationFn(n__1,V__NUMBER))
         =>
         ((s__MeasureFn(V__NUMBER,s__LongTon) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__2240)
          ,s__PoundMass))))))
)
)

Mid-level-ontology.kif 12820-12824
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       (((V__NUMBER = s__MultiplicationFn(n__1,V__NUMBER))
         =>
         ((s__MeasureFn(V__NUMBER,s__Nanometer) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__0_000000001)
          ,s__Meter))))))
)
)

Mid-level-ontology.kif 18115-18121
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       (((V__NUMBER = s__MultiplicationFn(n__1,V__NUMBER))
         =>
         ((s__MeasureFn(V__NUMBER,s__RegistryTon) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__100)
          ,s__CubicFoot))))))
)
)

Mid-level-ontology.kif 12859-12863
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       (((V__NUMBER = s__MultiplicationFn(n__1,V__NUMBER))
         =>
         ((s__MeasureFn(V__NUMBER,s__TonMass) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__2000)
          ,s__PoundMass))))))
)
)

Mid-level-ontology.kif 12793-12797
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       (((V__NUMBER = s__MultiplicationFn(n__1,V__NUMBER))
         =>
         ((s__MeasureFn(V__NUMBER,s__YardLength) = s__MeasureFn(s__MultiplicationFn(n__3,V__NUMBER)
          ,s__FootLength))))))
)
)

Mid-level-ontology.kif 18105-18109

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


( ! [V__AMOUNT,V__UNIT] :
   (((s__instance(V__AMOUNT,s__Number) &
         s__instance(V__AMOUNT,s__PhysicalQuantity))
       =>
       ((((s__instance(V__UNIT,s__UnitOfMeasure) &
               (V__AMOUNT = s__MeasureFn(n__1,s__SquareUnitFn(V__UNIT))))
         =>
         (V__AMOUNT = s__MultiplicationFn(s__MeasureFn(n__1,V__UNIT)
        ,s__MeasureFn(n__1,V__UNIT))))
&
((V__AMOUNT = s__MultiplicationFn(s__MeasureFn(n__1,V__UNIT)
  ,s__MeasureFn(n__1,V__UNIT)))
=>
(s__instance(V__UNIT,s__UnitOfMeasure) &
(V__AMOUNT = s__MeasureFn(n__1,s__SquareUnitFn(V__UNIT))))))))
)
)

Geography.kif 3804-3808 An unit of measure is an instance of unit of measure and a number is equal to 1 the square unit of the unit of measure(s) if and only if the number is equal to 1 the unit of measure(s) and 1 the unit of measure(s)
( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] :
   (((s__instance(V__NUMBER1,s__Integer) &
         s__instance(V__NUMBER2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       ((((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))
&
((s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1)
=>
(s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)))))
)
)

Merge.kif 4941-4943 An integer mod another integer is equal to a third integer if and only if (the largest integer less than or equal to the integer and the other integer and the other integer and the third integer) is equal to the integer
( ! [V__O,V__A] :
   (((s__instance(V__O,s__Physical) &
         s__instance(V__A,s__RealNumber))
       =>
       (((s__measure(V__O,s__MeasureFn(V__A,s__MetricTon))
           =>
           s__measure(V__O,s__MeasureFn(s__MultiplicationFn(V__A,n__2205)
        ,s__PoundMass)))
     &
     (s__measure(V__O,s__MeasureFn(s__MultiplicationFn(V__A,n__2205)
    ,s__PoundMass))
   =>
   s__measure(V__O,s__MeasureFn(V__A,s__MetricTon))))))
)
)

Mid-level-ontology.kif 12807-12813 The measure of a physical is a real number metric ton(s) if and only if the measure of the physical is the real number and 2205 pound mass(s)
( ! [V__OBJ,V__DEG] :
   (((s__instance(V__OBJ,s__Physical) &
         s__instance(V__DEG,s__RealNumber))
       =>
       (((s__measure(V__OBJ,s__MeasureFn(V__DEG,s__AngularDegree))
           =>
           s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(n__60,V__DEG)
        ,s__ArcMinute)))
     &
     (s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(n__60,V__DEG)
    ,s__ArcMinute))
   =>
   s__measure(V__OBJ,s__MeasureFn(V__DEG,s__AngularDegree))))))
)
)

Geography.kif 378-380 The measure of a physical is a real number angular degree(s) if and only if the measure of the physical is 60 and the real number arc minute(s)
( ! [V__OBJ,V__DEG] :
   (((s__instance(V__OBJ,s__Physical) &
         s__instance(V__DEG,s__RealNumber))
       =>
       (((s__measure(V__OBJ,s__MeasureFn(V__DEG,s__ArcMinute))
           =>
           s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(n__60,V__DEG)
        ,s__ArcSecond)))
     &
     (s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(n__60,V__DEG)
    ,s__ArcSecond))
   =>
   s__measure(V__OBJ,s__MeasureFn(V__DEG,s__ArcMinute))))))
)
)

Geography.kif 397-399 The measure of a physical is a real number arc minute(s) if and only if the measure of the physical is 60 and the real number arc second(s)
( ! [V__REGION,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__arableLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__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 2070-2080
No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 193-212
No TPTP formula. May not be expressible in strict first order. Geography.kif 658-668
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12768-12777
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12779-12788
( ! [V__VA,V__L,V__M] :
   (((s__instance(V__VA,s__Number) &
         s__instance(V__L,s__List) &
         s__instance(V__M,s__Number))
       =>
       ((((V__VA = s__VarianceAverageFn(V__M,V__L))
           &
           (n__1 = s__ListLengthFn(V__L)))
       =>
       ((V__VA = s__MultiplicationFn(s__SubtractionFn(V__M,s__ListOrderFn(V__L,n__1))
      ,s__SubtractionFn(V__M,s__ListOrderFn(V__L,n__1))))))))
)
)

Weather.kif 1485-1496
( ! [V__NUMBER] :
   (((s__instance(V__NUMBER,s__Integer) &
         ~((V__NUMBER = n__0)))
       =>
       ((n__1 = s__MultiplicationFn(V__NUMBER,s__ReciprocalFn(V__NUMBER)))))
)
)

Merge.kif 4923-4928
No TPTP formula. May not be expressible in strict first order. Cars.kif 3095-3109
( ! [V__WH,V__SWH,V__WW] :
   (((s__instance(V__WH,s__LengthMeasure) &
         s__instance(V__SWH,s__RealNumber))
       =>
       (((s__instance(V__WW,s__WaterWave) &
             s__waveHeight(V__WW,V__WH))
         =>
         (( ? [V__LIST, V__WA, V__U] :
             ((s__instance(V__LIST,s__List) &
                 (s__inList(V__WH,V__LIST)
                 &
                 s__instance(V__WA,s__WaterArea) &
                 s__eventLocated(V__WW,V__WA)
               &
               s__instance(V__U,s__LengthMeasure) &
               s__significantWaveHeight(V__WA,s__WhenFn(V__WW)
            ,s__MeasureFn(V__SWH,V__U))
         &
         (V__SWH = s__MultiplicationFn(n__4,s__StandardDeviationFn(V__LIST)))))))))))
)
)

Weather.kif 1531-1546
( ! [V__REGION,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__otherLandUseArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__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 2160-2172
( ! [V__REGION,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__permanentCropLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__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 2118-2128
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 2200-2210
( ! [V__N1,V__Time,V__N2,V__N3,V__TimeOfSplit,V__NewNumber,V__Stocks,V__TimeAfterSplit,V__Number] :
   (((s__instance(V__N1,s__Integer) &
         s__instance(V__Time,s__Agent) &
         s__instance(V__Time,s__TimeInterval) &
         s__instance(V__N2,s__Integer) &
         s__instance(V__N3,s__Number) &
         s__instance(V__TimeOfSplit,s__TimeInterval) &
         s__instance(V__NewNumber,s__RealNumber) &
         s__instance(V__Stocks,s__Physical) &
         s__instance(V__TimeAfterSplit,s__Agent) &
         s__instance(V__TimeAfterSplit,s__TimeInterval) &
         s__instance(V__Number,s__RealNumber))
       =>
       (((s__price(V__Stocks,s__MeasureFn(V__Number,s__UnitedStatesDollar),V__Time)
           &
           ( ? [V__Event] :
             ((s__instance(V__Event,s__StockSplit) &
                 (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 2212-2224
( ! [V__Amount,V__Period,V__Rate,V__Balance,V__Account,V__Rate_Decimal] :
   (((s__instance(V__Amount,s__Interest) &
         s__instance(V__Amount,s__Number) &
         s__instance(V__Period,s__TimeInterval) &
         s__instance(V__Rate,s__Number) &
         s__instance(V__Rate,s__PhysicalQuantity) &
         s__instance(V__Balance,s__Number) &
         s__instance(V__Balance,s__CurrencyMeasure) &
         s__instance(V__Account,s__FinancialAccount) &
         s__instance(V__Rate_Decimal,s__Number))
       =>
       (((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)
      ,n__100)))
=>
((V__Amount = s__MultiplicationFn(s__MultiplicationFn(s__MagnitudeFn(V__Period)
  ,V__Balance)
,V__Rate_Decimal))))))
)
)

FinancialOntology.kif 514-520
No TPTP formula. May not be expressible in strict first order. Merge.kif 17186-17212
( ! [V__U,V__F,V__H1,V__H2,V__S1,V__HF,V__S2] :
   (((s__instance(V__U,s__UnitOfMeasure) &
         s__instance(V__F,s__SelfConnectedObject) &
         s__instance(V__H1,s__RealNumber) &
         s__instance(V__H2,s__RealNumber) &
         s__instance(V__S1,s__SelfConnectedObject) &
         s__instance(V__HF,s__RealNumber) &
         s__instance(V__S2,s__SelfConnectedObject))
       =>
       ((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(n__2,V__HF))
&
s__greaterThan(V__H2,s__MultiplicationFn(n__2,V__HF)))))))
)
)

Mid-level-ontology.kif 2720-2731
( ! [V__U,V__F,V__H1,V__H2,V__S1,V__HF,V__S2] :
   (((s__instance(V__U,s__UnitOfMeasure) &
         s__instance(V__F,s__SelfConnectedObject) &
         s__instance(V__H1,s__RealNumber) &
         s__instance(V__H2,s__RealNumber) &
         s__instance(V__S1,s__SelfConnectedObject) &
         s__instance(V__HF,s__RealNumber) &
         s__instance(V__S2,s__SelfConnectedObject))
       =>
       ((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(n__3,V__HF))
&
s__lessThan(V__H2,s__MultiplicationFn(n__3,V__HF)))))))
)
)

Mid-level-ontology.kif 2739-2750
( ! [V__CIRCLE,V__LENGTH] :
   (((s__instance(V__CIRCLE,s__Circle) &
         s__instance(V__LENGTH,s__LengthMeasure))
       =>
       ((s__circumfrence(V__CIRCLE,V__LENGTH)
         =>
         (( ? [V__D, V__UNIT] :
             ((s__instance(V__D,s__RealNumber) &
                 s__instance(V__UNIT,s__UnitOfMeasure) &
                 (s__diameter(V__CIRCLE,s__MeasureFn(V__D,V__UNIT))
               &
               (s__MeasureFn(s__MultiplicationFn(V__D,n__3_14)
              ,V__UNIT)
             = V__LENGTH)))))))))
)
)

Mid-level-ontology.kif 30183-30191
( ! [V__CIRCLE,V__LENGTH] :
   (((s__instance(V__CIRCLE,s__Circle) &
         s__instance(V__LENGTH,s__LengthMeasure))
       =>
       ((s__diameter(V__CIRCLE,V__LENGTH)
         =>
         (( ? [V__NHALF, V__UHALF] :
             ((s__instance(V__NHALF,s__RealNumber) &
                 s__instance(V__UHALF,s__UnitOfMeasure) &
                 (s__radius(V__CIRCLE,s__MeasureFn(V__NHALF,V__UHALF))
               &
               (s__MeasureFn(s__MultiplicationFn(V__NHALF,n__2)
              ,V__UHALF)
             = V__LENGTH)))))))))
)
)

Merge.kif 7447-7452
( ! [V__C,V__U,V__L] :
   (((s__instance(V__C,s__Circle) &
         s__instance(V__U,s__UnitOfMeasure) &
         s__instance(V__L,s__RealNumber))
       =>
       (((s__DiameterFn(V__C)
           = s__MeasureFn(V__L,V__U))
       =>
       (( ? [V__R] :
           ((s__instance(V__R,s__RealNumber) &
               ((s__RadiusFn(V__C)
                 = s__MeasureFn(V__R,V__U))
             &
             (s__MultiplicationFn(V__R,n__2)
             = V__L)))))))))
)
)

Mid-level-ontology.kif 4651-4656

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


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

Mid-level-ontology.kif 12831-12837 1 Cubic foot(s) is equal to 1 foot length(s) and 1 foot length(s) and 1 foot length(s)
(s__MeasureFn(n__1,s__SquareKilometer) = s__MultiplicationFn(s__MeasureFn(n__1,s__KiloFn(s__Meter))
,s__MeasureFn(n__1,s__KiloFn(s__Meter))))

Geography.kif 624-625 1 Square kilometer(s) is equal to 1 1 thousand meters(s) and 1 1 thousand meters(s)
(s__MeasureFn(n__1,s__SquareMeter) = s__MultiplicationFn(s__MeasureFn(n__1,s__Meter),s__MeasureFn(n__1,s__Meter)))

Geography.kif 3792-3793 1 Square meter(s) is equal to 1 meter(s) and 1 meter(s)
( ! [V__DEG] :
   ((s__instance(V__DEG,s__RealNumber) =>
       ((s__MeasureFn(V__DEG,s__ArcMinute) = s__MeasureFn(s__MultiplicationFn(n__60,V__DEG)
        ,s__ArcSecond))))
   )
)

Geography.kif 402-402 A real number arc minute(s) is equal to 60 and the real number arc second(s)
( ! [V__NUM] :
   ((s__instance(V__NUM,s__RealNumber) =>
       ((s__MeasureFn(V__NUM,s__AngularDegree) = s__MeasureFn(s__MultiplicationFn(n__60,V__NUM)
        ,s__ArcMinute))))
   )
)

Geography.kif 383-383 A real number angular degree(s) is equal to 60 and the real number arc minute(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Amu) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__1_6605402E_24)
        ,s__Gram))))
   )
)

Merge.kif 6937-6939 A real number amu(s) is equal to the real number and 1.6605402E-24 gram(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Angstrom) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__1_0E_10)
        ,s__Meter))))
   )
)

Merge.kif 6959-6961 A real number angstrom(s) is equal to the real number and 1.0E-10 meter(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__AngularDegree) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,s__DivisionFn(s__Pi,n__180_0))
      ,s__Radian))))
)
)

Merge.kif 7153-7155 A real number angular degree(s) is equal to the real number and pi and 180.0 radian(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__BritishThermalUnit) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__1055_05585262)
        ,s__Joule))))
   )
)

Merge.kif 7139-7141 A real number british thermal unit(s) is equal to the real number and 1055.05585262 joule(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Byte) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__8)
        ,s__Bit))))
   )
)

Merge.kif 7211-7213 A real number byte(s) is equal to the real number and 8 bit(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Calorie) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__4_1868)
        ,s__Joule))))
   )
)

Merge.kif 7131-7133 A real number calorie(s) is equal to the real number and 4.1868 joule(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Centimeter) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__0_01)
        ,s__Meter))))
   )
)

Merge.kif 6570-6572 A real number centimeter(s) is equal to the real number and 0.01 meter(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__DayDuration) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__24)
        ,s__HourDuration))))
   )
)

Merge.kif 6877-6879 A real number day duration(s) is equal to the real number and 24 hour duration(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__ElectronVolt) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__1_60217733E_19)
        ,s__Joule))))
   )
)

Merge.kif 6947-6949 A real number electron volt(s) is equal to the real number and 1.60217733E-19 joule(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__EuroCent) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__0_01)
        ,s__EuroDollar))))
   )
)

Merge.kif 7191-7193 A real number euro cent(s) is equal to the real number and 0.01 euro dollar(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__FootLength) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__0_3048)
        ,s__Meter))))
   )
)

Merge.kif 6972-6974 A real number foot length(s) is equal to the real number and 0.3048 meter(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__HourDuration) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__60)
        ,s__MinuteDuration))))
   )
)

Merge.kif 6885-6887 A real number hour duration(s) is equal to the real number and 60 minute duration(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Inch) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__0_0254)
        ,s__Meter))))
   )
)

Merge.kif 6979-6981 A real number inch(s) is equal to the real number and 0.0254 meter(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__KiloByte) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__1024)
        ,s__Byte))))
   )
)

Merge.kif 7221-7223 A real number kilo byte(s) is equal to the real number and 1024 byte(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Kilogram) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__1000)
        ,s__Gram))))
   )
)

Merge.kif 7065-7068 A real number kilogram(s) is equal to the real number and 1000 gram(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Kilometer) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__1000)
        ,s__Meter))))
   )
)

Merge.kif 6589-6592 A real number kilometer(s) is equal to the real number and 1000 meter(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__MegaByte) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__1024)
        ,s__KiloByte))))
   )
)

Merge.kif 7231-7233 A real number mega byte(s) is equal to the real number and 1024 kilo byte(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Micrometer) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__0_0000001)
        ,s__Meter))))
   )
)

Geography.kif 6627-6630 A real number micrometer(s) is equal to the real number and 0.0000001 meter(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Mile) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__1609_344)
        ,s__Meter))))
   )
)

Merge.kif 6986-6988 A real number mile(s) is equal to the real number and 1609.344 meter(s)
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       ((s__MeasureFn(V__NUMBER,s__Millimeter) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__0_001)
        ,s__Meter))))
   )
)

Merge.kif 6579-6582 A real number millimeter(s) is equal to the real number and 0.001 meter(s)

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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