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).
Ontologie
SUMO / UNITS-OF-MEASUREClass(es)
Související termín(y)
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
Typy argumentů
konstantní veličina MeasureFn(reálné číslo, měrná jednotka)
Axiomy (71)
Jestliže "number unit(s)" se rovná quant a unit je podtřídou quanttype, potom quant je instancí třídy 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)))))
Jestliže unit je instancí třídy měrná jednotka, potom "kilo fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(KiloFn ?UNIT)
(MeasureFn 1000 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "mega fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MegaFn ?UNIT)
(MeasureFn 1000000 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "giga fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(GigaFn ?UNIT)
(MeasureFn 1000000000 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "tera fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(TeraFn ?UNIT)
(MeasureFn 1000000000000 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "milli fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MilliFn ?UNIT)
(MeasureFn 0.001 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "micro fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MicroFn ?UNIT)
(MeasureFn 0.000001 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "nano fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(NanoFn ?UNIT)
(MeasureFn 0.000000001 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "pico fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(PicoFn ?UNIT)
(MeasureFn 0.000000000001 ?UNIT)))
Jestliže number je instancí třídy reálné číslo a unit je instancí třídy měrná jednotka, potom "magnitude fn(number unit(s))" se rovná number.
(=>
(and
(instance ?NUMBER RealNumber)
(instance ?UNIT UnitOfMeasure))
(equal
(MagnitudeFn
(MeasureFn ?NUMBER ?UNIT))
?NUMBER))
Jestliže number je instancí třídy reálné číslo, potom "number centimeter(s)" se rovná ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Centimeter)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
Meter)))
Jestliže number je instancí třídy reálné číslo, potom "number celsius degree(s)" se rovná ""(number-)" kelvin degree(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER CelsiusDegree)
(MeasureFn
(SubtractionFn ?NUMBER 273.15)
KelvinDegree)))
Jestliže number je instancí třídy reálné číslo, potom "number celsius degree(s)" se rovná """(number-)"/" fahrenheit degree(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER CelsiusDegree)
(MeasureFn
(DivisionFn
(SubtractionFn ?NUMBER 32)
1.8)
FahrenheitDegree)))
Jestliže number je instancí třídy reálné číslo, potom "number day duration(s)" se rovná ""number*" hour duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER DayDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 24)
HourDuration)))
Jestliže number je instancí třídy reálné číslo, potom "number hour duration(s)" se rovná ""number*" minute duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER HourDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 60)
MinuteDuration)))
Jestliže number je instancí třídy reálné číslo, potom "number minute duration(s)" se rovná ""number*" second duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER MinuteDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 60)
SecondDuration)))
Jestliže number je instancí třídy reálné číslo, potom "number week duration(s)" se rovná ""number*" day duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER WeekDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 7)
DayDuration)))
Jestliže number je instancí třídy reálné číslo, potom "number year duration(s)" se rovná ""number*" day duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER YearDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 365)
DayDuration)))
Jestliže number je instancí třídy reálné číslo, potom "number amu(s)" se rovná ""number**" gram(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Amu)
(MeasureFn
(MultiplicationFn ?NUMBER 1.6605402 E-24)
Gram)))
Jestliže number je instancí třídy reálné číslo, potom "number electron volt(s)" se rovná ""number**" joule(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER ElectronVolt)
(MeasureFn
(MultiplicationFn ?NUMBER 1.60217733 E-19)
Joule)))
Jestliže number je instancí třídy reálné číslo, potom "number angstrom(s)" se rovná ""number**" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Angstrom)
(MeasureFn
(MultiplicationFn ?NUMBER 1.0 E-10)
Meter)))
Jestliže number je instancí třídy reálné číslo, potom "number foot(s)" se rovná ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Foot)
(MeasureFn
(MultiplicationFn ?NUMBER 0.3048)
Meter)))
Jestliže number je instancí třídy reálné číslo, potom "number inch(s)" se rovná ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Inch)
(MeasureFn
(MultiplicationFn ?NUMBER 0.0254)
Meter)))
Jestliže number je instancí třídy reálné číslo, potom "number mile(s)" se rovná ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Mile)
(MeasureFn
(MultiplicationFn ?NUMBER 1609.344)
Meter)))
Jestliže number je instancí třídy reálné číslo, potom "number united states gallon(s)" se rovná ""number*" liter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedStatesGallon)
(MeasureFn
(MultiplicationFn ?NUMBER 3.785411784)
Liter)))
Jestliže number je instancí třídy reálné číslo, potom "number quart(s)" se rovná ""number/" united states gallon(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Quart)
(MeasureFn
(DivisionFn ?NUMBER 4)
UnitedStatesGallon)))
Jestliže number je instancí třídy reálné číslo, potom "number pint(s)" se rovná ""number/" quart(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Pint)
(MeasureFn
(DivisionFn ?NUMBER 2)
Quart)))
Jestliže number je instancí třídy reálné číslo, potom "number cup(s)" se rovná ""number/" pint(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Cup)
(MeasureFn
(DivisionFn ?NUMBER 2)
Pint)))
Jestliže number je instancí třídy reálné číslo, potom "number ounce(s)" se rovná ""number/" cup(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Ounce)
(MeasureFn
(DivisionFn ?NUMBER 8)
Cup)))
Jestliže number je instancí třídy reálné číslo, potom "number united kingdom gallon(s)" se rovná ""number*" liter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedKingdomGallon)
(MeasureFn
(MultiplicationFn ?NUMBER 4.54609)
Liter)))
Jestliže number je instancí třídy reálné číslo, potom "number pound mass(s)" se rovná ""number*" gram(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER PoundMass)
(MeasureFn
(MultiplicationFn ?NUMBER 453.59237)
Gram)))
Jestliže number je instancí třídy reálné číslo, potom "number slug(s)" se rovná ""number*" gram(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Slug)
(MeasureFn
(MultiplicationFn ?NUMBER 14593.90)
Gram)))
Jestliže number je instancí třídy reálné číslo, potom "number rankine degree(s)" se rovná ""number*" kelvin degree(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER RankineDegree)
(MeasureFn
(MultiplicationFn ?NUMBER 1.8)
KelvinDegree)))
Jestliže number je instancí třídy reálné číslo, potom "number pound force(s)" se rovná ""number*" newton(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER PoundForce)
(MeasureFn
(MultiplicationFn ?NUMBER 4.448222)
Newton)))
Jestliže number je instancí třídy reálné číslo, potom "number calorie(s)" se rovná ""number*" joule(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Calorie)
(MeasureFn
(MultiplicationFn ?NUMBER 4.1868)
Joule)))
Jestliže number je instancí třídy reálné číslo, potom "number british thermal unit(s)" se rovná ""number*" joule(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER BritishThermalUnit)
(MeasureFn
(MultiplicationFn ?NUMBER 1055.05585262)
Joule)))
Jestliže number je instancí třídy reálné číslo, potom "number angular degree(s)" se rovná ""number*"pi/"" radian(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER AngularDegree)
(MeasureFn
(MultiplicationFn
?NUMBER
(DivisionFn Pi 180))
Radian)))
Jestliže number je instancí třídy reálné číslo, potom "number united states cent(s)" se rovná ""number*" united states dollar(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedStatesCent)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
UnitedStatesDollar)))
Jestliže number je instancí třídy reálné číslo, potom "number euro cent(s)" se rovná ""number*" euro dollar(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER EuroCent)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
EuroDollar)))
Jestliže number je instancí třídy reálné číslo, potom "number byte(s)" se rovná ""number*" bit(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Byte)
(MeasureFn
(MultiplicationFn ?NUMBER 8)
Bit)))
Jestliže number je instancí třídy reálné číslo, potom "number kilo byte(s)" se rovná ""number*" byte(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER KiloByte)
(MeasureFn
(MultiplicationFn ?NUMBER 1024)
Byte)))
Jestliže number je instancí třídy reálné číslo, potom "number mega byte(s)" se rovná ""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))))
Jestliže year je instancí třídy rok, potom duration of year je " year duration(s)".
(=>
(instance ?YEAR Year)
(duration
?YEAR
(MeasureFn 1 YearDuration)))
Jestliže leap je instancí třídy přestupný rok a leap se rovná "number rok(s)", potom
(=>
(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)))
Jestliže month je instancí třídy leden, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH January)
(duration
?MONTH
(MeasureFn 31 DayDuration)))
Jestliže "únor of year" se rovná month a year není instancí třídy přestupný rok, potom duration of month je " day duration(s)".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(not
(instance ?YEAR LeapYear)))
(duration
?MONTH
(MeasureFn 28 DayDuration)))
Jestliže "únor of year" se rovná month a year je instancí třídy přestupný rok, potom duration of month je " day duration(s)".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(instance ?YEAR LeapYear))
(duration
?MONTH
(MeasureFn 29 DayDuration)))
Jestliže month je instancí třídy březen, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH March)
(duration
?MONTH
(MeasureFn 31 DayDuration)))
Jestliže month je instancí třídy duben, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH April)
(duration
?MONTH
(MeasureFn 30 DayDuration)))
Jestliže month je instancí třídy květen, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH May)
(duration
?MONTH
(MeasureFn 31 DayDuration)))
Jestliže month je instancí třídy červen, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH June)
(duration
?MONTH
(MeasureFn 30 DayDuration)))
Jestliže month je instancí třídy červenec, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH July)
(duration
?MONTH
(MeasureFn 31 DayDuration)))
Jestliže month je instancí třídy srpen, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH August)
(duration
?MONTH
(MeasureFn 31 DayDuration)))
Jestliže month je instancí třídy září, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH September)
(duration
?MONTH
(MeasureFn 30 DayDuration)))
Jestliže month je instancí třídy říjen, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH October)
(duration
?MONTH
(MeasureFn 31 DayDuration)))
Jestliže month je instancí třídy listopad, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH November)
(duration
?MONTH
(MeasureFn 30 DayDuration)))
Jestliže month je instancí třídy prosinec, potom duration of month je " day duration(s)".
(=>
(instance ?MONTH December)
(duration
?MONTH
(MeasureFn 31 DayDuration)))
Jestliže day je instancí třídy den, potom duration of day je " day duration(s)".
(=>
(instance ?DAY Day)
(duration
?DAY
(MeasureFn 1 DayDuration)))
Jestliže week je instancí třídy týren, potom duration of week je " week duration(s)".
(=>
(instance ?WEEK Week)
(duration
?WEEK
(MeasureFn 1 WeekDuration)))
Jestliže hour je instancí třídy hodina, potom duration of hour je " hour duration(s)".
(=>
(instance ?HOUR Hour)
(duration
?HOUR
(MeasureFn 1 HourDuration)))
Jestliže minute je instancí třídy minuta, potom duration of minute je " minute duration(s)".
(=>
(instance ?MINUTE Minute)
(duration
?MINUTE
(MeasureFn 1 MinuteDuration)))
Jestliže second je instancí třídy vteřina, potom duration of second je " second duration(s)".
(=>
(instance ?SECOND Second)
(duration
?SECOND
(MeasureFn 1 SecondDuration)))
Jestliže month je instancí třídy měsíc a duration of month je "number day duration(s)", potom "cardinality fn(decomposition of month into ? dens)" se rovná number.
(=>
(and
(instance ?MONTH Month)
(duration
?MONTH
(MeasureFn ?NUMBER DayDuration)))
(equal
(CardinalityFn
(TemporalCompositionFn ?MONTH Day))
?NUMBER))
Jestliže increase je instancí třídy zvyšování parametru a obj je účastníkem increase, potom existují unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence increase a "obj unit(s)" se rovná quant2 právě po doba existence increase a quant2 je větší než 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))))
Jestliže heat je instancí třídy zahřívání a obj je účastníkem heat, potom existují jednotka teploty unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence heat a "obj unit(s)" se rovná quant2 právě po doba existence heat a quant2 je větší než 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))))
Jestliže decrease je instancí třídy snižování parametru a obj je účastníkem decrease, potom existují unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence decrease a "obj unit(s)" se rovná quant2 právě po doba existence decrease a quant2 je menší než 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))))
Jestliže cool je instancí třídy ochlazování a obj je účastníkem cool, potom existují jednotka teploty unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence cool a "obj unit(s)" se rovná quant2 právě po doba existence cool a quant2 je menší než 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))))
Jestliže meas je instancí třídy měření a agent je původcem meas a obj je účastníkem meas, potom existují quant,unit tak, že agent knows "the measure of obj je "quant unit(s)"" právě po doba existence 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))))))
