Browsing Interface : Welcome guest : log in 		[  Home |  Graph |  LogLearn |  Editor |  ]  KB:  Language: 
  Formal Language: 

KB Term:  Term intersection
English Word: 

Sigma KEE - MeasureFn
MeasureFn

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


s__instance(s__MeasureFn,s__BinaryFunction)

 Merge.kif 6465-6465 Measure is an instance of binary function
s__instance(s__MeasureFn,s__TotalValuedRelation)

 Merge.kif 6466-6466 Measure is an instance of total valued relation
s__domain(s__MeasureFn,n__1,s__RealNumber)

 Merge.kif 6467-6467 The number 1 argument of measure is an instance of real number
s__domain(s__MeasureFn,n__2,s__UnitOfMeasure)

 Merge.kif 6468-6468 The number 2 argument of measure is an instance of unit of measure
s__range(s__MeasureFn,s__PhysicalQuantity)

 Merge.kif 6469-6469 The range of measure is an instance of physical quantity
s__documentation(s__MeasureFn, s__EnglishLanguage, "This BinaryFunction maps a RealNumber and a UnitOfMeasure to that Number of units_ It is used to express `measured instances of PhysicalQuantity_ Example: the concept of three meters is represented as (MeasureFn 3 Meter)_") Merge.kif 6471-6475 The range of measure is an instance of physical quantity

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


s__termFormat(s__EnglishLanguage, s__MeasureFn, "measure") domainEnglishFormat.kif 36671-36671
s__termFormat(s__ChineseTraditionalLanguage, s__MeasureFn, "測量") domainEnglishFormat.kif 36672-36672
s__termFormat(s__ChineseLanguage, s__MeasureFn, "测量") domainEnglishFormat.kif 36673-36673
s__format(s__EnglishLanguage, s__MeasureFn, "%1 %2(s)") english_format.kif 636-636

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


! [V__N,V__QUANT,V__UNIT] :
((s__instance(V__N,s__RealNumber) =>
     ((s__instance(V__QUANT,s__MeasureFn(V__N,V__UNIT))
     &
     s__instance(V__UNIT,s__CompositeUnitOfMeasure))
   =>
   s__instance(V__QUANT,s__FunctionQuantity)))
)

 Merge.kif 6344-6348 If X is an instance of Y Z(s) and Z is an instance of composite unit of measure, then X is an instance of function quantity
! [V__N,V__QUANT,V__UNIT] :
((s__instance(V__N,s__RealNumber) =>
     ((s__instance(V__QUANT,s__MeasureFn(V__N,V__UNIT))
     &
     s__instance(V__UNIT,s__NonCompositeUnitOfMeasure))
   =>
   s__instance(V__QUANT,s__ConstantQuantity)))
)

 Merge.kif 6350-6354 If X is an instance of Y Z(s) and Z is an instance of non composite unit of measure, then X is an instance of constant quantity
! [V__NUMBER,V__QUANT,V__UNIT] :
(((s__instance(V__NUMBER,s__RealNumber) &
       s__instance(V__QUANT,s__PhysicalQuantity))
     =>
     (((s__MeasureFn(V__NUMBER,V__UNIT)
         = V__QUANT)
       &
       s__instance(V__UNIT,s__UnitOfLength))
     =>
     s__instance(V__QUANT,s__LengthMeasure)))
)

 Merge.kif 6477-6481 If equal X Y(s) and Z and Y is an instance of unit of length, then Z is an instance of length measure
! [V__NUMBER,V__QUANT,V__UNIT] :
(((s__instance(V__NUMBER,s__RealNumber) &
       s__instance(V__QUANT,s__PhysicalQuantity))
     =>
     (((s__MeasureFn(V__NUMBER,V__UNIT)
         = V__QUANT)
       &
       s__instance(V__UNIT,s__UnitOfMass))
     =>
     s__instance(V__QUANT,s__MassMeasure)))
)

 Merge.kif 6483-6487 If equal X Y(s) and Z and Y is an instance of unit of mass, then Z is an instance of mass measure
! [V__NUMBER,V__QUANT,V__UNIT] :
(((s__instance(V__NUMBER,s__RealNumber) &
       s__instance(V__QUANT,s__PhysicalQuantity))
     =>
     (((s__MeasureFn(V__NUMBER,V__UNIT)
         = V__QUANT)
       &
       s__instance(V__UNIT,s__UnitOfArea))
     =>
     s__instance(V__QUANT,s__AreaMeasure)))
)

 Merge.kif 6489-6493 If equal X Y(s) and Z and Y is an instance of unit of area, then Z is an instance of area measure
! [V__NUMBER,V__QUANT,V__UNIT] :
(((s__instance(V__NUMBER,s__RealNumber) &
       s__instance(V__QUANT,s__PhysicalQuantity))
     =>
     (((s__MeasureFn(V__NUMBER,V__UNIT)
         = V__QUANT)
       &
       s__instance(V__UNIT,s__UnitOfVolume))
     =>
     s__instance(V__QUANT,s__VolumeMeasure)))
)

 Merge.kif 6495-6499 If equal X Y(s) and Z and Y is an instance of unit of volume, then Z is an instance of volume measure
! [V__NUMBER,V__QUANT,V__UNIT] :
(((s__instance(V__NUMBER,s__RealNumber) &
       s__instance(V__QUANT,s__PhysicalQuantity))
     =>
     (((s__MeasureFn(V__NUMBER,V__UNIT)
         = V__QUANT)
       &
       s__instance(V__UNIT,s__UnitOfTemperature))
     =>
     s__instance(V__QUANT,s__TemperatureMeasure)))
)

 Merge.kif 6501-6505 If equal X Y(s) and Z and Y is an instance of unit of temperature, then Z is an instance of temperature measure
! [V__NUMBER,V__QUANT,V__UNIT] :
(((s__instance(V__NUMBER,s__RealNumber) &
       s__instance(V__QUANT,s__PhysicalQuantity))
     =>
     (((s__MeasureFn(V__NUMBER,V__UNIT)
         = V__QUANT)
       &
       s__instance(V__UNIT,s__UnitOfCurrency))
     =>
     s__instance(V__QUANT,s__CurrencyMeasure)))
)

 Merge.kif 6507-6511 If equal X Y(s) and Z and Y is an instance of unit of currency, then Z is an instance of currency measure
! [V__NUMBER,V__QUANT,V__UNIT] :
(((s__instance(V__NUMBER,s__RealNumber) &
       s__instance(V__QUANT,s__PhysicalQuantity))
     =>
     (((s__MeasureFn(V__NUMBER,V__UNIT)
         = V__QUANT)
       &
       s__instance(V__UNIT,s__UnitOfAngularMeasure))
     =>
     s__instance(V__QUANT,s__AngleMeasure)))
)

 Merge.kif 6513-6517 If equal X Y(s) and Z and Y is an instance of unit of angular measure, then Z is an instance of angle measure
! [V__NUMBER,V__QUANT,V__UNIT] :
(((s__instance(V__NUMBER,s__RealNumber) &
       s__instance(V__QUANT,s__PhysicalQuantity))
     =>
     (((s__MeasureFn(V__NUMBER,V__UNIT)
         = V__QUANT)
       &
       s__instance(V__UNIT,s__UnitOfDuration))
     =>
     s__instance(V__QUANT,s__TimeDuration)))
)

 Merge.kif 6519-6523 If equal X Y(s) and Z and Y is an instance of unit of duration, then Z is an instance of time duration
! [V__NUMBER,V__QUANT,V__UNIT] :
(((s__instance(V__NUMBER,s__RealNumber) &
       s__instance(V__QUANT,s__PhysicalQuantity))
     =>
     (((s__MeasureFn(V__NUMBER,V__UNIT)
         = V__QUANT)
       &
       s__instance(V__UNIT,s__UnitOfInformation))
     =>
     s__instance(V__QUANT,s__InformationMeasure)))
)

 Merge.kif 6525-6529 If equal X Y(s) and Z and Y is an instance of unit of information, then Z is an instance of information measure
! [V__NUMBER,V__QUANT,V__UNIT] :
((s__instance(V__NUMBER,s__RealNumber) =>
     ((s__instance(V__QUANT,s__PhysicalQuantity) &
         s__instance(V__UNIT,s__UnitOfMeasure) &
         (V__QUANT = s__MeasureFn(V__NUMBER,V__UNIT)))
     =>
     (s__UnitFn(V__QUANT)
     = V__UNIT)))
)

 Merge.kif 6739-6745 If X is an instance of physical quantity, Y is an instance of unit of measure, and equal X and Z Y(s), then equal the unit of X and Y
! [V__NUMBER,V__QUANT,V__UNIT] :
(((s__instance(V__NUMBER,s__RealNumber) &
       s__instance(V__QUANT,s__PhysicalQuantity))
     =>
     (((s__MeasureFn(V__NUMBER,V__UNIT)
         = V__QUANT)
       &
       s__instance(V__UNIT,s__UnitOfFrequency))
     =>
     s__instance(V__QUANT,s__FrequencyMeasure)))
)

 Merge.kif 6965-6969 If equal X Y(s) and Z and Y is an instance of unit of frequency, then Z is an instance of frequency measure
! [V__QUANTITY,V__NUMBER] :
(((s__instance(V__QUANTITY,s__PhysicalQuantity) &
       s__instance(V__NUMBER,s__RealNumber))
     =>
     ((V__QUANTITY = s__MeasureFn(V__NUMBER,s__Coulomb))
       =>
       s__instance(V__QUANTITY,s__TimeDependentQuantity)))
   )

 Merge.kif 7039-7041 If equal X and Y coulomb(s), then X is an instance of time dependent quantity
! [V__QUANTITY,V__NUMBER] :
(((s__instance(V__QUANTITY,s__PhysicalQuantity) &
       s__instance(V__NUMBER,s__RealNumber))
     =>
     ((V__QUANTITY = s__MeasureFn(V__NUMBER,s__Becquerel))
       =>
       s__instance(V__QUANTITY,s__TimeDependentQuantity)))
   )

 Merge.kif 7167-7169 If equal X and Y becquerel(s), then X is an instance of time dependent quantity
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     ((s__MeasureFn(n__1,s__MonthDuration) = s__MeasureFn(V__NUMBER,s__DayDuration))
       =>
       s__greaterThanOrEqualTo(V__NUMBER,n__28)))
)

 Merge.kif 7241-7245 If equal 1 month duration(s) and X day duration(s), then X is greater than or equal to 28
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     ((s__MeasureFn(n__1,s__MonthDuration) = s__MeasureFn(V__NUMBER,s__DayDuration))
       =>
       s__lessThanOrEqualTo(V__NUMBER,n__31)))
)

 Merge.kif 7247-7251 If equal 1 month duration(s) and X day duration(s), then X is less than or equal to 31
! [V__QUANT,V__N] :
(((s__instance(V__QUANT,s__PhysicalQuantity) &
       s__instance(V__N,s__RealNumber))
     =>
     ((V__QUANT = s__MeasureFn(V__N,s__AngularDegree))
       =>
       s__instance(V__QUANT,s__PlaneAngleMeasure)))
   )

 Merge.kif 7501-7503 If equal X and Y angular degree(s), then X is an instance of plane angle measure
! [V__ANGLE,V__NUMBER] :
(((s__instance(V__ANGLE,s__Physical) &
       s__instance(V__NUMBER,s__RealNumber))
     =>
     (s__measure(V__ANGLE,s__MeasureFn(V__NUMBER,s__AngularDegree))
     =>
     (s__greaterThanOrEqualTo(V__NUMBER,n__0_0)
     &
     s__lessThanOrEqualTo(V__NUMBER,n__360_0))))
)

 Merge.kif 7509-7513 If the measure of X is Y angular degree(s), then Y is greater than or equal to 0.0 and Y is less than or equal to 360.0
! [V__O,V__M,V__U] :
(((s__instance(V__O,s__Physical) &
       s__instance(V__M,s__RealNumber) &
       s__instance(V__U,s__UnitOfMeasure))
     =>
     (s__length(V__O,s__MeasureFn(V__M,V__U))
   =>
   ~((? [V__M2] :
       ((s__instance(V__M2,s__RealNumber) &
           (s__linearExtent(V__O,s__MeasureFn(V__M2,V__U))
         &
         s__greaterThan(V__M2,V__M))))))))
)

 Merge.kif 7706-7714 If the length of X is Y Z(s), then there doesn't exist W such that the linear extent of X is W Z(s) and W is greater than Y
! [V__S,V__CO,V__N,V__U,V__SI,V__N2] :
(((s__instance(V__S,s__Class) &
       s__subclass(V__S,s__Substance) &
       s__instance(V__CO,s__CorpuscularObject) &
       s__instance(V__N,s__RealNumber) &
       s__instance(V__U,s__UnitOfMass) &
       s__instance(V__SI,s__Object) &
       s__instance(V__N2,s__RealNumber))
     =>
     ((s__amount(V__S,V__CO,s__MeasureFn(V__N,V__U))
     &
     s__instance(V__SI,V__S)
   &
   s__measure(V__SI,s__MeasureFn(V__N2,V__U))
&
s__part(V__SI,V__CO))
=>
(? [V__L] :
((s__instance(V__L,s__List) &
(s__inList(s__MeasureFn(V__N2,V__U)
,V__L)
&
(V__L = s__AmountsFn(V__S,V__CO,V__U))
&
(V__N = s__ListSumFn(V__L))))))))
)

 Merge.kif 7740-7755 If amount X, Y and Z W(s), V is an instance of X, the measure of V is U W(s), and V is a part of Y, then there exists T such that U W(s) is a member of T and equal T and Amounts fn X, Y and W and equal Z and the sum of T
! [V__NUMBER,V__MONTH] :
((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 9688-9692 If X is an instance of month and duration of X is Y day duration(s), then equal the number of instances in decomposition of X into days and Y
! [V__PROCESS,V__PATH1,V__SOURCE,V__DEST,V__MEASURE1,V__U,V__DISTANCE,V__OBJ] :
(((s__instance(V__PROCESS,s__Motion) &
       s__instance(V__PATH1,s__Object) &
       s__instance(V__SOURCE,s__Object) &
       s__instance(V__DEST,s__Object) &
       s__instance(V__MEASURE1,s__RealNumber) &
       s__instance(V__U,s__UnitOfMeasure) &
       s__instance(V__DISTANCE,s__RealNumber) &
       s__instance(V__OBJ,s__Object))
     =>
     ((s__path(V__PROCESS,V__PATH1)
       &
       s__origin(V__PROCESS,V__SOURCE)
     &
     s__destination(V__PROCESS,V__DEST)
   &
   s__length(V__PATH1,s__MeasureFn(V__MEASURE1,V__U))
&
s__distance(V__SOURCE,V__DEST,s__MeasureFn(V__DISTANCE,V__U))
&
~(s__greaterThan(V__MEASURE1,V__DISTANCE))
&
s__part(V__OBJ,V__PATH1))
=>
s__between(V__SOURCE,V__OBJ,V__DEST)))
)

 Merge.kif 11334-11344 If All of the following hold: (1) X is path along which Y occurs (2) Y originates at Z (3) Y ends up at W (4) the length of X is V U(s) (5) the distance between Z and W is T U(s) (6) V is not greater than T (7) S is a part of X, then S is between Z and W
! [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)))))
)

 Merge.kif 11532-11538 equal X and Y miles per hour(s) if and only if equal X and Y mile(s) per 1 hour duration(s)

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


! [V__G,V__M,V__PN,V__PA,V__N,V__AN,V__AA] :
(((s__instance(V__G,s__Graph) &
       s__instance(V__M,s__UnitOfMeasure) &
       s__instance(V__PN,s__Physical) &
       s__instance(V__PA,s__Physical) &
       s__instance(V__N,s__RealNumber))
     =>
     ((s__graphMeasure(V__G,V__M)
       &
       s__instance(V__AN,s__GraphNode) &
       s__graphPart(V__AN,V__G)
     &
     s__graphPart(V__AA,V__G)
   &
   s__instance(V__AA,s__GraphArc) &
   s__abstractCounterpart(V__AN,V__PN)
&
s__abstractCounterpart(V__AA,V__PA)
&
s__arcWeight(V__AA,V__N))
=>
s__measure(V__PA,s__MeasureFn(V__N,V__M))))
)

 Merge.kif 6284-6295 If All of the following hold: (1) X is the unit in Y (2) Z is an instance of graph node (3) Z is a part of Y (4) W is a part of Y (5) W is an instance of graph arc (6) the abstract counterpart of V is Z (7) the abstract counterpart of U is W (8) the value of W is T, then the measure of U is T X(s)
! [V__KILOUNIT,V__UNIT] :
((s__instance(V__KILOUNIT,s__UnitOfMeasure) =>
     ((s__instance(V__UNIT,s__UnitOfMeasure) &
         (V__KILOUNIT = s__KiloFn(V__UNIT)))
     =>
     (s__MeasureFn(n__1,V__KILOUNIT)
     = s__MeasureFn(n__1000,V__UNIT))))
)

 Merge.kif 6594-6598 If X is an instance of unit of measure and equal Y and 1 thousand Z, then equal 1 Y(s) and 1000 X(s)
! [V__MEGAUNIT,V__UNIT] :
((s__instance(V__MEGAUNIT,s__UnitOfMeasure) =>
     ((s__instance(V__UNIT,s__UnitOfMeasure) &
         (V__MEGAUNIT = s__MegaFn(V__UNIT)))
     =>
     (s__MeasureFn(n__1,V__MEGAUNIT)
     = s__MeasureFn(n__1000000,V__UNIT))))
)

 Merge.kif 6608-6612 If X is an instance of unit of measure and equal Y and 1 million Z, then equal 1 Y(s) and 1000000 X(s)
! [V__GIGAUNIT,V__UNIT] :
((s__instance(V__GIGAUNIT,s__UnitOfMeasure) =>
     ((s__instance(V__UNIT,s__UnitOfMeasure) &
         (V__GIGAUNIT = s__GigaFn(V__UNIT)))
     =>
     (s__MeasureFn(n__1,V__GIGAUNIT)
     = s__MeasureFn(n__1000000,s__KiloFn(V__UNIT)))))
)

 Merge.kif 6622-6626 If X is an instance of unit of measure and equal Y and 1 billion Z, then equal 1 Y(s) and 1000000 1 thousand Z(s)
! [V__TERAUNIT,V__UNIT] :
((s__instance(V__TERAUNIT,s__UnitOfMeasure) =>
     ((s__instance(V__UNIT,s__UnitOfMeasure) &
         (V__TERAUNIT = s__TeraFn(V__UNIT)))
     =>
     (s__MeasureFn(n__1,V__TERAUNIT)
     = s__MeasureFn(n__1000000000,s__KiloFn(V__UNIT)))))
)

 Merge.kif 6636-6640 If X is an instance of unit of measure and equal Y and 1 trillion Z, then equal 1 Y(s) and 1000000000 1 thousand Z(s)
! [V__MILLIUNIT,V__UNIT] :
((s__instance(V__MILLIUNIT,s__UnitOfMeasure) =>
     ((s__instance(V__UNIT,s__UnitOfMeasure) &
         (V__MILLIUNIT = s__MilliFn(V__UNIT)))
     =>
     (s__MeasureFn(n__1,V__MILLIUNIT)
     = s__MeasureFn(n__0_001,V__UNIT))))
)

 Merge.kif 6650-6654 If X is an instance of unit of measure and equal Y and one thousandth of a X, then equal 1 Y(s) and 0.001 X(s)
! [V__MICROUNIT,V__UNIT] :
((s__instance(V__MICROUNIT,s__UnitOfMeasure) =>
     ((s__instance(V__UNIT,s__UnitOfMeasure) &
         (V__MICROUNIT = s__MicroFn(V__UNIT)))
     =>
     (s__MeasureFn(n__1,V__MICROUNIT)
     = s__MeasureFn(n__0_000001,V__UNIT))))
)

 Merge.kif 6664-6668 If X is an instance of unit of measure and equal Y and one millionth of a X, then equal 1 Y(s) and 0.000001 X(s)
! [V__NANOUNIT,V__UNIT] :
((s__instance(V__NANOUNIT,s__UnitOfMeasure) =>
     ((s__instance(V__UNIT,s__UnitOfMeasure) &
         (V__NANOUNIT = s__NanoFn(V__UNIT)))
     =>
     (s__MeasureFn(n__1,V__NANOUNIT)
     = s__MeasureFn(n__0_000000001,V__UNIT))))
)

 Merge.kif 6679-6683 If X is an instance of unit of measure and equal Y and one billionth of a X, then equal 1 Y(s) and 0.000000001 X(s)
! [V__PICOUNIT,V__UNIT] :
((s__instance(V__PICOUNIT,s__UnitOfMeasure) =>
     ((s__instance(V__UNIT,s__UnitOfMeasure) &
         (V__PICOUNIT = s__PicoFn(V__UNIT)))
     =>
     (s__MeasureFn(n__1,V__PICOUNIT)
     = s__MeasureFn(n__0_000000000001,V__UNIT))))
)

 Merge.kif 6694-6698 If X is an instance of unit of measure and equal Y and one trillionth of a X, then equal 1 Y(s) and 0.000000000001 X(s)
! [V__N] :
((s__instance(V__N,s__RealNumber) =>
     (s__MeasureFn(V__N,s__Horsepower) = s__MeasureFn(s__MultiplicationFn(V__N,n__746)
    ,s__Watt)))
)

 Merge.kif 7021-7025 If X is an instance of real number, then equal X horsepower(s) and X and 746 watt(s)
! [V__O,V__M,V__U] :
(((s__instance(V__O,s__Physical) &
       s__instance(V__M,s__RealNumber) &
       s__instance(V__U,s__UnitOfMeasure))
     =>
     (s__length(V__O,s__MeasureFn(V__M,V__U))
   =>
   ~((? [V__M2] :
       ((s__instance(V__M2,s__RealNumber) &
           (s__linearExtent(V__O,s__MeasureFn(V__M2,V__U))
         &
         s__greaterThan(V__M2,V__M))))))))
)

 Merge.kif 7706-7714 If the length of X is Y Z(s), then there doesn't exist W such that the linear extent of X is W Z(s) and W is greater than Y
! [V__S,V__CO,V__N,V__U,V__SI,V__N2] :
(((s__instance(V__S,s__Class) &
       s__subclass(V__S,s__Substance) &
       s__instance(V__CO,s__CorpuscularObject) &
       s__instance(V__N,s__RealNumber) &
       s__instance(V__U,s__UnitOfMass) &
       s__instance(V__SI,s__Object) &
       s__instance(V__N2,s__RealNumber))
     =>
     ((s__amount(V__S,V__CO,s__MeasureFn(V__N,V__U))
     &
     s__instance(V__SI,V__S)
   &
   s__measure(V__SI,s__MeasureFn(V__N2,V__U))
&
s__part(V__SI,V__CO))
=>
(? [V__L] :
((s__instance(V__L,s__List) &
(s__inList(s__MeasureFn(V__N2,V__U)
,V__L)
&
(V__L = s__AmountsFn(V__S,V__CO,V__U))
&
(V__N = s__ListSumFn(V__L))))))))
)

 Merge.kif 7740-7755 If amount X, Y and Z W(s), V is an instance of X, the measure of V is U W(s), and V is a part of Y, then there exists T such that U W(s) is a member of T and equal T and Amounts fn X, Y and W and equal Z and the sum of T
! [V__CIRCLE,V__LENGTH] :
(((s__instance(V__CIRCLE,s__Circle) &
       s__instance(V__CIRCLE,s__ClosedTwoDimensionalFigure) &
       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 7842-7847 If the diameter of X is Y, then there exist Z and W such that the radius of X is Z W(s) and equal Z and 2 W(s) and Y
! [V__OBJ1,V__OBJ2] :
(((s__instance(V__OBJ1,s__Object) &
       s__instance(V__OBJ2,s__Object))
     =>
     ((s__larger(V__OBJ1,V__OBJ2)
       =>
       (! [V__QUANT1,V__QUANT2,V__UNIT] :
         (((s__instance(V__QUANT1,s__RealNumber) &
               s__instance(V__QUANT2,s__RealNumber))
             =>
             ((s__measure(V__OBJ1,s__MeasureFn(V__QUANT1,V__UNIT))
             &
             s__measure(V__OBJ2,s__MeasureFn(V__QUANT2,V__UNIT))
         &
         s__instance(V__UNIT,s__UnitOfLength))
       =>
       s__greaterThan(V__QUANT1,V__QUANT2))))))
&
((! [V__QUANT1,V__QUANT2,V__UNIT] :
(((s__instance(V__QUANT1,s__RealNumber) &
     s__instance(V__QUANT2,s__RealNumber))
   =>
   ((s__measure(V__OBJ1,s__MeasureFn(V__QUANT1,V__UNIT))
   &
   s__measure(V__OBJ2,s__MeasureFn(V__QUANT2,V__UNIT))
&
s__instance(V__UNIT,s__UnitOfLength))
=>
s__greaterThan(V__QUANT1,V__QUANT2)))))
=>
s__larger(V__OBJ1,V__OBJ2))))
)

 Merge.kif 7937-7945 X is larger than Y if and only if Z, W and V the measure of X is Z V(s) and the measure of Y is W V(s) and V is an instance of unit of lengthZ is greater than W
! [V__YEAR] :
((s__instance(V__YEAR,s__Year) =>
     s__duration(V__YEAR,s__MeasureFn(n__1,s__YearDuration)))
)

 Merge.kif 8946-8948 If X is an instance of year, then duration of X is 1 year duration(s)
! [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 8961-8965 If equal X, 1, and X, then equal X decade duration(s) and X and 10 year duration(s)
! [V__D] :
((s__instance(V__D,s__Decade) =>
     s__duration(V__D,s__MeasureFn(n__1,s__DecadeDuration)))
)

 Merge.kif 8972-8974 If X is an instance of decade, then duration of X is 1 decade duration(s)
! [V__D] :
((s__instance(V__D,s__Decade) =>
     s__duration(V__D,s__MeasureFn(n__10,s__YearDuration)))
)

 Merge.kif 8976-8978 If X is an instance of decade, then duration of X is 10 year duration(s)
! [V__Q] :
((s__instance(V__Q,s__QuarterYear) =>
     s__duration(V__Q,s__MeasureFn(n__3,s__MonthDuration)))
)

 Merge.kif 9193-9195 If X is an instance of quarter year, then duration of X is 3 month duration(s)
! [V__MONTH] :
((s__instance(V__MONTH,s__January) =>
     s__duration(V__MONTH,s__MeasureFn(n__31,s__DayDuration)))
)

 Merge.kif 9254-9256 If X is an instance of January, then duration of X is 31 day duration(s)
! [V__MONTH,V__YEAR,V__Y] :
(((s__instance(V__MONTH,s__TimeInterval) &
       s__instance(V__YEAR,s__Class) &
       s__subclass(V__YEAR,s__Year))
     =>
     ((s__instance(V__MONTH,s__MonthFn(s__February,V__YEAR))
     &
     s__instance(V__Y,V__YEAR)
   &
   ~(s__instance(V__Y,s__LeapYear)))
=>
s__duration(V__MONTH,s__MeasureFn(n__28,s__DayDuration))))
)

 Merge.kif 9268-9273 If X is an instance of the month February, Y is an instance of Z, and Y is not an instance of leap year, then duration of X is 28 day duration(s)
! [V__MONTH,V__YEAR,V__Y] :
(((s__instance(V__MONTH,s__TimeInterval) &
       s__instance(V__YEAR,s__Class) &
       s__subclass(V__YEAR,s__Year))
     =>
     ((s__instance(V__MONTH,s__MonthFn(s__February,V__YEAR))
     &
     s__instance(V__Y,V__YEAR)
   &
   s__instance(V__Y,s__LeapYear))
=>
s__duration(V__MONTH,s__MeasureFn(n__29,s__DayDuration))))
)

 Merge.kif 9275-9280 If X is an instance of the month February, Y is an instance of Z, and Y is an instance of leap year, then duration of X is 29 day duration(s)
! [V__MONTH] :
((s__instance(V__MONTH,s__March) =>
     s__duration(V__MONTH,s__MeasureFn(n__31,s__DayDuration)))
)

 Merge.kif 9292-9294 If X is an instance of March, then duration of X is 31 day duration(s)
! [V__MONTH] :
((s__instance(V__MONTH,s__April) =>
     s__duration(V__MONTH,s__MeasureFn(n__30,s__DayDuration)))
)

 Merge.kif 9306-9308 If X is an instance of April, then duration of X is 30 day duration(s)
! [V__MONTH] :
((s__instance(V__MONTH,s__May) =>
     s__duration(V__MONTH,s__MeasureFn(n__31,s__DayDuration)))
)

 Merge.kif 9320-9322 If X is an instance of May, then duration of X is 31 day duration(s)

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


! [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 6899-6901 equal X centimeter(s) and X and 0.01 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 6908-6911 equal X millimeter(s) and X and 0.001 meter(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 6918-6921 equal X kilometer(s) and X and 1000 meter(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__CelsiusDegree) = s__MeasureFn(s__SubtractionFn(V__NUMBER,n__273_15)
    ,s__KelvinDegree)))
)

 Merge.kif 7127-7129 equal X celsius degree(s) and (X and 273.15) kelvin degree(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__CelsiusDegree) = s__MeasureFn(s__DivisionFn(s__SubtractionFn(V__NUMBER,n__32_0)
    ,n__1_8)
  ,s__FahrenheitDegree)))
)

 Merge.kif 7131-7133 equal X celsius degree(s) and (X and 32.0) and 1.8 fahrenheit degree(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 7206-7208 equal X day duration(s) and X and 24 hour duration(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 7214-7216 equal X hour duration(s) and X and 60 minute duration(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__MinuteDuration) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__60)
    ,s__SecondDuration)))
)

 Merge.kif 7222-7224 equal X minute duration(s) and X and 60 second duration(s)
s__MeasureFn(n__1,s__WeekDuration) = s__MeasureFn(n__7,s__DayDuration)

 Merge.kif 7231-7233 equal 1 week duration(s) and 7 day duration(s)
s__MeasureFn(n__1,s__YearDuration) = s__MeasureFn(n__365,s__DayDuration)

 Merge.kif 7258-7260 equal 1 year duration(s) and 365 day duration(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__Amu) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,s__DivisionFn(s__DivisionFn(s__DivisionFn(s__DivisionFn(n__1_6605402,n__1000000_0)
    ,n__1000000_0)
  ,n__1000000_0)
,n__1000000_0))
,s__Gram)))
)

 Merge.kif 7271-7281 equal X amu(s) and X and 1.6605402 and 1000000.0 and 1000000.0 and 1000000.0 and 1000000.0 gram(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__ElectronVolt) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,s__DivisionFn(s__DivisionFn(s__DivisionFn(n__1_60217733,n__1000000_0)
    ,n__1000000_0)
  ,n__10000000_0))
,s__Joule)))
)

 Merge.kif 7289-7297 equal X electron volt(s) and X and 1.60217733 and 1000000.0 and 1000000.0 and 10000000.0 joule(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__Angstrom) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,s__DivisionFn(s__DivisionFn(n__1_0,n__100000_0)
    ,n__100000_0))
,s__Meter)))
)

 Merge.kif 7307-7313 equal X angstrom(s) and X and 1.0 and 100000.0 and 100000.0 meter(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 7324-7326 equal X foot length(s) and X and 0.3048 meter(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 7331-7333 equal X inch(s) and X and 0.0254 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 7338-7340 equal X mile(s) and X and 1609.344 meter(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__UnitedStatesGallon) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__3_785411784)
    ,s__Liter)))
)

 Merge.kif 7350-7352 equal X united states gallon(s) and X and 3.785411784 liter(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__Quart) = s__MeasureFn(s__DivisionFn(V__NUMBER,n__4)
    ,s__UnitedStatesGallon)))
)

 Merge.kif 7359-7361 equal X quart(s) and X and 4 united states gallon(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__Pint) = s__MeasureFn(s__DivisionFn(V__NUMBER,n__2)
    ,s__Quart)))
)

 Merge.kif 7368-7370 equal X pint(s) and X and 2 quart(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__Cup) = s__MeasureFn(s__DivisionFn(V__NUMBER,n__2)
    ,s__Pint)))
)

 Merge.kif 7377-7379 equal X cup(s) and X and 2 pint(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__Ounce) = s__MeasureFn(s__DivisionFn(V__NUMBER,n__8)
    ,s__Cup)))
)

 Merge.kif 7386-7388 equal X ounce(s) and X and 8 cup(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__UnitedKingdomGallon) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__4_54609)
    ,s__Liter)))
)

 Merge.kif 7395-7397 equal X united kingdom gallon(s) and X and 4.54609 liter(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 7417-7420 equal X kilogram(s) and X and 1000 gram(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__PoundMass) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__453_59237)
    ,s__Gram)))
)

 Merge.kif 7434-7436 equal X pound mass(s) and X and 453.59237 gram(s)
! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__Slug) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__14593_90)
    ,s__Gram)))
)

 Merge.kif 7442-7444 equal X slug(s) and X and 14593.90 gram(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.0-ac69cf7a (2026-05-13) is open source software produced by Articulate Software and its partners