SUMO   View all facts   Glossary   Help

Entity > Abstract > Class > Relation > Function > BinaryFunction > MeasureFn

MeasureFn
subject			fact

MeasureFn	documentation 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)
	has axiom (=> (and (equal (MeasureFn ?NUMBER ?UNIT) ?QUANT) (subclass ?UNIT ?QUANTTYPE) (not (equal ?QUANTTYPE UnitOfMeasure))) (subclass ?QUANT ?QUANTTYPE))
	has axiom (=> (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))))
	has axiom (=> (and (instance ?FUNCTION RelationExtendedToQuantities) (instance ?FUNCTION BinaryFunction) (instance ?NUMBER1 RealNumber) (instance ?NUMBER2 RealNumber) (equal (AssignmentFn ?FUNCTION ?NUMBER1 ?NUMBER2) ?VALUE)) (forall (?UNIT) (=> (instance ?UNIT UnitOfMeasure) (equal (AssignmentFn ?FUNCTION (MeasureFn ?NUMBER1 ?UNIT) (MeasureFn ?NUMBER2 ?UNIT)) (MeasureFn ?VALUE ?UNIT)))))
	has axiom (=> (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))))
	has axiom (=> (and (instance ?MEAS Measuring) (agent ?MEAS ?AGENT) (patient ?MEAS ?OBJ)) (exists (?QUANT ?UNIT) (holdsDuring (ImmediateFutureFn (WhenFn ?MEAS)) (knows ?AGENT (measure ?OBJ (MeasureFn ?QUANT ?UNIT))))))
	has axiom (=> (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)))))
	has axiom (=> (larger ?OBJ1 ?OBJ2) (forall (?QUANT1 ?QUANT2) (=> (and (measure ?OBJ1 (MeasureFn ?QUANT1 LengthMeasure)) (measure ?OBJ2 (MeasureFn ?QUANT2 LengthMeasure))) (greaterThan ?QUANT1 ?QUANT2))))
	has axiom (equal (MagnitudeFn (MeasureFn ?NUMBER ?UNIT)) ?NUMBER)
	has axiom (equal (MeasureFn ?NUMBER GigaHertz) (MeasureFn (MultiplicationFn ?NUMBER 1.0E9) Hertz))
	has axiom (equal (MeasureFn ?NUMBER Amu) (MeasureFn (MultiplicationFn ?NUMBER 1.6605402E-27) Kilogram))
	has axiom (equal (MeasureFn ?NUMBER Angstrom) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-10) Meter))
	has axiom (equal (MeasureFn ?NUMBER BritishThermalUnit) (MeasureFn (MultiplicationFn ?NUMBER 1055.05585262) Joule))
	has axiom (equal (MeasureFn ?NUMBER Byte) (MeasureFn (MultiplicationFn ?NUMBER 8) Bit))
	has axiom (equal (MeasureFn ?NUMBER Calorie) (MeasureFn (MultiplicationFn ?NUMBER 4.1868) Joule))
	has axiom (equal (MeasureFn ?NUMBER Celsius) (MeasureFn (SubtractionFn ?NUMBER 273.15) Kelvin))
	has axiom (equal (MeasureFn ?NUMBER Centimeter) (MeasureFn (MultiplicationFn ?NUMBER 0.01) Meter))
	has axiom (equal (MeasureFn ?NUMBER CentUnitedStates) (MeasureFn (MultiplicationFn ?NUMBER .01) DollarUnitedStates))
	has axiom (equal (MeasureFn ?NUMBER Cup) (MeasureFn (DivisionFn ?NUMBER 2) Pint))
	has axiom (equal (MeasureFn ?NUMBER ElectronVolt) (MeasureFn (MultiplicationFn ?NUMBER 1.60217733E-19) Joule))
	has axiom (equal (MeasureFn ?NUMBER Foot) (MeasureFn (MultiplicationFn ?NUMBER 0.3048) Meter))
	has axiom (equal (MeasureFn ?NUMBER Inch) (MeasureFn (MultiplicationFn ?NUMBER 0.0254) Meter))
	has axiom (equal (MeasureFn ?NUMBER KiloByte) (MeasureFn (MultiplicationFn ?NUMBER 1024) Byte))
	has axiom (equal (MeasureFn ?NUMBER MegaByte) (MeasureFn (MultiplicationFn ?NUMBER 1024) KiloByte))
	has axiom (equal (MeasureFn ?NUMBER MegaHertz) (MeasureFn (MultiplicationFn ?NUMBER 1.0E6) Hertz))
	has axiom (equal (MeasureFn ?NUMBER Mile) (MeasureFn (MultiplicationFn ?NUMBER 1609.344) Meter))
	has axiom (equal (MeasureFn ?NUMBER MinuteDuration) (MeasureFn (MultiplicationFn ?NUMBER 60) SecondDuration))
	has axiom (equal (MeasureFn ?NUMBER Ounce) (MeasureFn (DivisionFn ?NUMBER 8) Cup))
	has axiom (equal (MeasureFn ?NUMBER Pint) (MeasureFn (DivisionFn ?NUMBER 2) Quart))
	has axiom (equal (MeasureFn ?NUMBER Pound) (MeasureFn (MultiplicationFn ?NUMBER 0.45359237) Kilogram))
	has axiom (equal (MeasureFn ?NUMBER PoundForce) (MeasureFn (MultiplicationFn ?NUMBER 4.448222) Newton))
	has axiom (equal (MeasureFn ?NUMBER Quart) (MeasureFn (DivisionFn ?NUMBER 4) UnitedStatesGallon))
	has axiom (equal (MeasureFn ?NUMBER Rankine) (MeasureFn (MultiplicationFn ?NUMBER 1.8) Kelvin))
	has axiom (equal (MeasureFn ?NUMBER Slug) (MeasureFn (MultiplicationFn ?NUMBER 14.59390) Kilogram))
	has axiom (equal (MeasureFn ?NUMBER UnitedKingdomGallon) (MeasureFn (MultiplicationFn ?NUMBER 4.54609) Liter))
	has axiom (equal (MeasureFn ?NUMBER UnitedStatesGallon) (MeasureFn (MultiplicationFn ?NUMBER 3.785411784) Liter))
	has axiom (equal (MeasureFn ?NUMBER AngularDegree) (MeasureFn (MultiplicationFn ?NUMBER (DivisionFn Pi 180)) Radian))
	has axiom (equal (MeasureFn ?NUMBER DayDuration) (MeasureFn (MultiplicationFn ?NUMBER 24) HourDuration))
	has axiom (equal (MeasureFn ?NUMBER Gram) (MeasureFn (MultiplicationFn ?NUMBER 0.001) Kilogram))
	has axiom (equal (MeasureFn ?NUMBER HourDuration) (MeasureFn (MultiplicationFn ?NUMBER 60) MinuteDuration))
	has axiom (equal (MeasureFn ?NUMBER Kilogram) (MeasureFn (MultiplicationFn ?NUMBER 1000) Gram))
	has axiom (equal (MeasureFn ?NUMBER KiloHertz) (MeasureFn (MultiplicationFn ?NUMBER 1000) Hertz))
	has axiom (equal (MeasureFn ?NUMBER Kilometer) (MeasureFn (MultiplicationFn ?NUMBER 1000) Meter))
	has axiom (equal (MeasureFn ?NUMBER KiloWatt) (MeasureFn (MultiplicationFn ?NUMBER 1000) Watt))
	has axiom (equal (MeasureFn ?NUMBER MegaOhm) (MeasureFn (MultiplicationFn ?NUMBER 1.0E6) Ohm))
	has axiom (equal (MeasureFn ?NUMBER MegaPascal) (MeasureFn (MultiplicationFn ?NUMBER 1.0E6) Pascal))
	has axiom (equal (MeasureFn ?NUMBER MicroOhm) (MeasureFn (MultiplicationFn ?NUMBER 0.000001) Ohm))
	has axiom (equal (MeasureFn ?NUMBER MicroVolt) (MeasureFn (MultiplicationFn ?NUMBER 0.000001) Volt))
	has axiom (equal (MeasureFn ?NUMBER MilliAmpere) (MeasureFn (MultiplicationFn ?NUMBER .001) Ampere))
	has axiom (equal (MeasureFn ?NUMBER MilliVolt) (MeasureFn (MultiplicationFn ?NUMBER .001) Volt))
	has axiom (equal (MeasureFn ?NUMBER NanoAmpere) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-9) Ampere))
	has axiom (equal (MeasureFn ?NUMBER NanoSecond) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-9) Second))
	has axiom (equal (MeasureFn ?NUMBER PicoAmpere) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-12) Ampere))
	has axiom (equal (MeasureFn ?NUMBER PicoSecond) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-12) SecondDuration))
	has axiom (equal (MeasureFn ?NUMBER YearDuration) (MeasureFn (MultiplicationFn ?NUMBER 365) DayDuration))
	has domain1 RealNumber
	has domain2 UnitOfMeasure
	has range ConstantQuantity
	is an instance of BinaryFunction
BinaryFunction	is first domain of distributes
	is first domain of identityElement
	is second domain of distributes
Class	is third domain of domain
	is third domain of domainSubclass
Abstract	is disjoint from Physical

Next BinaryFunction: MereologicalDifferenceFn    Up: BinaryFunction    Previous BinaryFunction: LogFn