Select language: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi
Concept:
English word:
Home

measure fn (MeasureFn)

This BinaryFunction maps a RealNumber and a UnitOfMeasure to that Number of units. It is used for expressing ConstantQuantities. For example, the concept of three meters is represented as (MeasureFn 3 Meter).

Ontology

SUMO / UNITS-OF-MEASURE

Class(es)

class
is instance of
  inheritable relation  
is instance of
  binary function  
is instance of
  measure fn  

Coordinate term(s)

addition fn  day fn  density fn  division fn  edition fn  exponentiation fn  graph path fn  hour fn  intersection fn  interval fn  kappa fn  list concatenate fn  list order fn  log fn  max fn  maximal weighted path fn  mereological difference fn  mereological product fn  mereological sum fn  min fn  minimal weighted path fn  minute fn  month fn  multiplication fn  periodical issue fn  recurrent time interval fn  relative complement fn  relative time fn  remainder fn  second fn  series volume fn  speed fn  subtraction fn  temporal composition fn  time interval fn  union fn  where fn 

Type restrictions

constant quantity MeasureFn(real number, unit of measure)

Axioms (71)

If "number unit(s)" is equal to quant and unit is a subclass of quanttype, then quant is an instance of quanttype.
(=>
      (and
            (equal
                  (MeasureFn ?NUMBER ?UNIT)
                  ?QUANT)
            (subclass ?UNIT ?QUANTTYPE))
      (instance ?QUANT ?QUANTTYPE))

(=>
      (and
            (instance ?REL RelationExtendedToQuantities)
            (instance ?REL TernaryRelation)
            (instance ?NUMBER1 RealNumber)
            (instance ?NUMBER2 RealNumber)
            (holds ?REL ?NUMBER1 ?NUMBER2 ?VALUE))
      (forall
            (?UNIT)
            (=>
                  (instance ?UNIT UnitOfMeasure)
                  (holds
                        ?REL
                        (MeasureFn ?NUMBER1 ?UNIT)
                        (MeasureFn ?NUMBER2 ?UNIT)
                        (MeasureFn ?VALUE ?UNIT)))))

(=>
      (and
            (instance ?REL RelationExtendedToQuantities)
            (instance ?REL BinaryRelation)
            (instance ?NUMBER1 RealNumber)
            (instance ?NUMBER2 RealNumber)
            (holds ?REL ?NUMBER1 ?NUMBER2))
      (forall
            (?UNIT)
            (=>
                  (instance ?UNIT UnitOfMeasure)
                  (holds
                        ?REL
                        (MeasureFn ?NUMBER1 ?UNIT)
                        (MeasureFn ?NUMBER2 ?UNIT)))))

If unit is an instance of unit of measure, then "1 thousand units" is equal to " unit(s)".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (KiloFn ?UNIT)
            (MeasureFn 1000 ?UNIT)))

If unit is an instance of unit of measure, then "1 million units" is equal to " unit(s)".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MegaFn ?UNIT)
            (MeasureFn 1000000 ?UNIT)))

If unit is an instance of unit of measure, then "1 billion units " is equal to " unit(s)".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (GigaFn ?UNIT)
            (MeasureFn 1000000000 ?UNIT)))

If unit is an instance of unit of measure, then "1 trillion units" is equal to " unit(s)".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (TeraFn ?UNIT)
            (MeasureFn 1000000000000 ?UNIT)))

If unit is an instance of unit of measure, then "one thousandth of a unit" is equal to " unit(s)".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MilliFn ?UNIT)
            (MeasureFn 0.001 ?UNIT)))

If unit is an instance of unit of measure, then "one millionth of a unit" is equal to " unit(s)".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MicroFn ?UNIT)
            (MeasureFn 0.000001 ?UNIT)))

If unit is an instance of unit of measure, then "one billionth of a unit" is equal to " unit(s)".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (NanoFn ?UNIT)
            (MeasureFn 0.000000001 ?UNIT)))

If unit is an instance of unit of measure, then "one trillionth of a unit" is equal to " unit(s)".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (PicoFn ?UNIT)
            (MeasureFn 0.000000000001 ?UNIT)))

If number is an instance of real number and unit is an instance of unit of measure, then "the magnitude of "number unit(s)"" is equal to number.
(=>
      (and
            (instance ?NUMBER RealNumber)
            (instance ?UNIT UnitOfMeasure))
      (equal
            (MagnitudeFn
                  (MeasureFn ?NUMBER ?UNIT))
            ?NUMBER))

If number is an instance of real number, then "number centimeter(s)" is equal to ""number*" meter(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Centimeter)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  Meter)))

If number is an instance of real number, then "number celsius degree(s)" is equal to ""(number-)" kelvin degree(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER CelsiusDegree)
            (MeasureFn
                  (SubtractionFn ?NUMBER 273.15)
                  KelvinDegree)))

If number is an instance of real number, then "number celsius degree(s)" is equal to """(number-)"/" fahrenheit degree(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER CelsiusDegree)
            (MeasureFn
                  (DivisionFn
                        (SubtractionFn ?NUMBER 32)
                        1.8)
                  FahrenheitDegree)))

If number is an instance of real number, then "number day duration(s)" is equal to ""number*" hour duration(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER DayDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 24)
                  HourDuration)))

If number is an instance of real number, then "number hour duration(s)" is equal to ""number*" minute duration(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER HourDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 60)
                  MinuteDuration)))

If number is an instance of real number, then "number minute duration(s)" is equal to ""number*" second duration(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER MinuteDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 60)
                  SecondDuration)))

If number is an instance of real number, then "number week duration(s)" is equal to ""number*" day duration(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER WeekDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 7)
                  DayDuration)))

If number is an instance of real number, then "number year duration(s)" is equal to ""number*" day duration(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER YearDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 365)
                  DayDuration)))

If number is an instance of real number, then "number amu(s)" is equal to ""number**" gram(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Amu)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.6605402 E-24)
                  Gram)))

If number is an instance of real number, then "number electron volt(s)" is equal to ""number**" joule(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER ElectronVolt)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.60217733 E-19)
                  Joule)))

If number is an instance of real number, then "number angstrom(s)" is equal to ""number**" meter(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Angstrom)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.0 E-10)
                  Meter)))

If number is an instance of real number, then "number foot(s)" is equal to ""number*" meter(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Foot)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.3048)
                  Meter)))

If number is an instance of real number, then "number inch(s)" is equal to ""number*" meter(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Inch)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.0254)
                  Meter)))

If number is an instance of real number, then "number mile(s)" is equal to ""number*" meter(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Mile)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1609.344)
                  Meter)))

If number is an instance of real number, then "number united states gallon(s)" is equal to ""number*" liter(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedStatesGallon)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 3.785411784)
                  Liter)))

If number is an instance of real number, then "number quart(s)" is equal to ""number/" united states gallon(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Quart)
            (MeasureFn
                  (DivisionFn ?NUMBER 4)
                  UnitedStatesGallon)))

If number is an instance of real number, then "number pint(s)" is equal to ""number/" quart(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Pint)
            (MeasureFn
                  (DivisionFn ?NUMBER 2)
                  Quart)))

If number is an instance of real number, then "number cup(s)" is equal to ""number/" pint(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Cup)
            (MeasureFn
                  (DivisionFn ?NUMBER 2)
                  Pint)))

If number is an instance of real number, then "number ounce(s)" is equal to ""number/" cup(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Ounce)
            (MeasureFn
                  (DivisionFn ?NUMBER 8)
                  Cup)))

If number is an instance of real number, then "number united kingdom gallon(s)" is equal to ""number*" liter(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedKingdomGallon)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.54609)
                  Liter)))

If number is an instance of real number, then "number pound mass(s)" is equal to ""number*" gram(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER PoundMass)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 453.59237)
                  Gram)))

If number is an instance of real number, then "number slug(s)" is equal to ""number*" gram(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Slug)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 14593.90)
                  Gram)))

If number is an instance of real number, then "number rankine degree(s)" is equal to ""number*" kelvin degree(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER RankineDegree)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.8)
                  KelvinDegree)))

If number is an instance of real number, then "number pound force(s)" is equal to ""number*" newton(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER PoundForce)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.448222)
                  Newton)))

If number is an instance of real number, then "number calorie(s)" is equal to ""number*" joule(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Calorie)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.1868)
                  Joule)))

If number is an instance of real number, then "number british thermal unit(s)" is equal to ""number*" joule(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER BritishThermalUnit)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1055.05585262)
                  Joule)))

If number is an instance of real number, then "number angular degree(s)" is equal to ""number*"pi/"" radian(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER AngularDegree)
            (MeasureFn
                  (MultiplicationFn
                        ?NUMBER
                        (DivisionFn Pi 180))
                  Radian)))

If number is an instance of real number, then "number united states cent(s)" is equal to ""number*" united states dollar(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedStatesCent)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  UnitedStatesDollar)))

If number is an instance of real number, then "number euro cent(s)" is equal to ""number*" euro dollar(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER EuroCent)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  EuroDollar)))

If number is an instance of real number, then "number byte(s)" is equal to ""number*" bit(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Byte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 8)
                  Bit)))

If number is an instance of real number, then "number kilo byte(s)" is equal to ""number*" byte(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER KiloByte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1024)
                  Byte)))

If number is an instance of real number, then "number mega byte(s)" is equal to ""number*" kilo byte(s)".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER MegaByte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1024)
                  KiloByte)))

(=>
      (larger ?OBJ1 ?OBJ2)
      (forall
            (?QUANT1 ?QUANT2)
            (=>
                  (and
                        (measure
                              ?OBJ1
                              (MeasureFn ?QUANT1 LengthMeasure))
                        (measure
                              ?OBJ2
                              (MeasureFn ?QUANT2 LengthMeasure)))
                  (greaterThan ?QUANT1 ?QUANT2))))

If year is an instance of year, then duration of year is " year duration(s)".
(=>
      (instance ?YEAR Year)
      (duration
            ?YEAR
            (MeasureFn 1 YearDuration)))

If leap is an instance of leap year and leap is equal to "number year(s)", then
(=>
      (and
            (instance ?LEAP LeapYear)
            (equal
                  ?LEAP
                  (MeasureFn ?NUMBER Year)))
      (or
            (and
                  (equal
                        (RemainderFn ?NUMBER 4)
                        0)
                  (not
                        (equal
                              (RemainderFn ?NUMBER 100)
                              0)))
            (equal
                  (RemainderFn ?NUMBER 400)
                  0)))

If month is an instance of january, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH January)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If "the month february" is equal to month and year is not an instance of leap year, then duration of month is " day duration(s)".
(=>
      (and
            (equal
                  (MonthFn February ?YEAR)
                  ?MONTH)
            (not
                  (instance ?YEAR LeapYear)))
      (duration
            ?MONTH
            (MeasureFn 28 DayDuration)))

If "the month february" is equal to month and year is an instance of leap year, then duration of month is " day duration(s)".
(=>
      (and
            (equal
                  (MonthFn February ?YEAR)
                  ?MONTH)
            (instance ?YEAR LeapYear))
      (duration
            ?MONTH
            (MeasureFn 29 DayDuration)))

If month is an instance of march, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH March)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month is an instance of april, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH April)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month is an instance of may, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH May)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month is an instance of june, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH June)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month is an instance of july, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH July)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month is an instance of august, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH August)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month is an instance of september, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH September)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month is an instance of october, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH October)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month is an instance of november, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH November)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month is an instance of december, then duration of month is " day duration(s)".
(=>
      (instance ?MONTH December)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If day is an instance of day, then duration of day is " day duration(s)".
(=>
      (instance ?DAY Day)
      (duration
            ?DAY
            (MeasureFn 1 DayDuration)))

If week is an instance of week, then duration of week is " week duration(s)".
(=>
      (instance ?WEEK Week)
      (duration
            ?WEEK
            (MeasureFn 1 WeekDuration)))

If hour is an instance of hour, then duration of hour is " hour duration(s)".
(=>
      (instance ?HOUR Hour)
      (duration
            ?HOUR
            (MeasureFn 1 HourDuration)))

If minute is an instance of minute, then duration of minute is " minute duration(s)".
(=>
      (instance ?MINUTE Minute)
      (duration
            ?MINUTE
            (MeasureFn 1 MinuteDuration)))

If second is an instance of second, then duration of second is " second duration(s)".
(=>
      (instance ?SECOND Second)
      (duration
            ?SECOND
            (MeasureFn 1 SecondDuration)))

If month is an instance of month and duration of month is "number day duration(s)", then "the number of instances in "decomposition of month into ? days"" is equal to number.
(=>
      (and
            (instance ?MONTH Month)
            (duration
                  ?MONTH
                  (MeasureFn ?NUMBER DayDuration)))
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MONTH Day))
            ?NUMBER))

If increase is an instance of increasing and obj is a patient of increase, then there exist unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of increase" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of increase" and quant2 is greater than quant1.
(=>
      (and
            (instance ?INCREASE Increasing)
            (patient ?INCREASE ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?INCREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?INCREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (greaterThan ?QUANT2 ?QUANT1))))

If heat is an instance of heating and obj is a patient of heat, then there exist temperature measure unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of heat" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of heat" and quant2 is greater than quant1.
(=>
      (and
            (instance ?HEAT Heating)
            (patient ?HEAT ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (instance ?UNIT TemperatureMeasure)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?HEAT))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?HEAT))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (greaterThan ?QUANT2 ?QUANT1))))

If decrease is an instance of decreasing and obj is a patient of decrease, then there exist unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of decrease" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of decrease" and quant2 is less than quant1.
(=>
      (and
            (instance ?DECREASE Decreasing)
            (patient ?DECREASE ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?DECREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?DECREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (lessThan ?QUANT2 ?QUANT1))))

If cool is an instance of cooling and obj is a patient of cool, then there exist temperature measure unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of cool" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of cool" and quant2 is less than quant1.
(=>
      (and
            (instance ?COOL Cooling)
            (patient ?COOL ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (instance ?UNIT TemperatureMeasure)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?COOL))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?COOL))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (lessThan ?QUANT2 ?QUANT1))))

If meas is an instance of measuring and meas is an agent of agent and obj is a patient of meas, then there exist quant,unit so that agent knows "the measure of obj is "quant unit(s)"" immediately after "the time of existence of meas".
(=>
      (and
            (instance ?MEAS Measuring)
            (agent ?MEAS ?AGENT)
            (patient ?MEAS ?OBJ))
      (exists
            (?QUANT ?UNIT)
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?MEAS))
                  (knows
                        ?AGENT
                        (measure
                              ?OBJ
                              (MeasureFn ?QUANT ?UNIT))))))