real number (RealNumber)

Any Number that can be expressed as a (possibly infinite) decimal, i.e. any Number that has a position on the number line.

Ontology

SUMO / BASE-ONTOLOGY

Superclass(es)

entity

abstract

quantity

number

real number

Subclass(es)

rational number irrational number nonnegative real number negative real number binary number

Coordinate term(s)

complex number imaginary number

Constrains relations

absolute value fn arc cosine fn arc sine fn arc tangent fn ceiling fn cosine fn denominator fn floor fn integer square root fn log fn magnitude fn measure fn numerator fn path weight fn probability fn real number fn signum fn sine fn square root fn tangent fn arc weight conditional probability

Related WordNet synsets

real number, real: any rational or irrational number

See more related synsets on a separate page.

Axioms (49)

number is exhaustively partitioned into real number,imaginary number,complex number.

(partition Number RealNumber ImaginaryNumber ComplexNumber)

less than is trichotomizing on real number.

(trichotomizingOn lessThan RealNumber)

greater than is trichotomizing on real number.

(trichotomizingOn greaterThan RealNumber)

less than or equal to is trichotomizing on real number.

(trichotomizingOn lessThanOrEqualTo RealNumber)

greater than or equal to is trichotomizing on real number.

(trichotomizingOn greaterThanOrEqualTo RealNumber)

real number is exhaustively partitioned into negative real number,nonnegative real number.

(partition RealNumber NegativeRealNumber NonnegativeRealNumber)

real number is exhaustively partitioned into rational number,irrational number.

(partition RealNumber RationalNumber IrrationalNumber)

If number is an instance of imaginary number, then there exists real number real so that number is equal to "real*"the square root of "".

(=>
      (instance ?NUMBER ImaginaryNumber)
      (exists
            (?REAL)
            (and
                  (instance ?REAL RealNumber)
                  (equal
                        ?NUMBER
                        (MultiplicationFn
                              ?REAL
                              (SquareRootFn -1))))))

number is an instance of nonnegative real number if and only if number is greater than or equal to and number is an instance of real number.

(<=>
      (instance ?NUMBER NonnegativeRealNumber)
      (and
            (greaterThanOrEqualTo ?NUMBER 0)
            (instance ?NUMBER RealNumber)))

number is an instance of positive real number if and only if number is greater than and number is an instance of real number.

(<=>
      (instance ?NUMBER PositiveRealNumber)
      (and
            (greaterThan ?NUMBER 0)
            (instance ?NUMBER RealNumber)))

number is an instance of negative real number if and only if number is less than and number is an instance of real number.

(<=>
      (instance ?NUMBER NegativeRealNumber)
      (and
            (lessThan ?NUMBER 0)
            (instance ?NUMBER RealNumber)))

complex number is disjoint from real number.

(disjoint ComplexNumber RealNumber)

If number is an instance of complex number, then there exist real number real1,real number real2 so that number is equal to "(real1+"real2*"the square root of "")".

(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?REAL1 ?REAL2)
            (and
                  (instance ?REAL1 RealNumber)
                  (instance ?REAL2 RealNumber)
                  (equal
                        ?NUMBER
                        (AdditionFn
                              ?REAL1
                              (MultiplicationFn
                                    ?REAL2
                                    (SquareRootFn -1)))))))

"the absolute value of number1" is equal to number2 and number1 is an instance of real number and number2 is an instance of real number if and only if

number1 is an instance of nonnegative real number and number1 is equal to number2
number1 is an instance of negative real number and number2 is equal to "(-number1)"

(<=>
      (and
            (equal
                  (AbsoluteValueFn ?NUMBER1)
                  ?NUMBER2)
            (instance ?NUMBER1 RealNumber)
            (instance ?NUMBER2 RealNumber))
      (or
            (and
                  (instance ?NUMBER1 NonnegativeRealNumber)
                  (equal ?NUMBER1 ?NUMBER2))
            (and
                  (instance ?NUMBER1 NegativeRealNumber)
                  (equal
                        ?NUMBER2
                        (SubtractionFn 0 ?NUMBER1)))))

if rel is an instance of relation extended to quantities and rel is an instance of ternary relation and number1 is an instance of real number and number2 is an instance of real number and rel(number1,number2,value) holds,
then for all unit holds: if unit is an instance of unit of measure, then rel("number1 unit(s)","number2 unit(s)","value unit(s)") holds

(=>
      (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)))))

if rel is an instance of relation extended to quantities and rel is an instance of binary relation and number1 is an instance of real number and number2 is an instance of real number and rel(number1,number2) holds,
then for all unit holds: if unit is an instance of unit of measure, then rel("number1 unit(s)","number2 unit(s)") holds

(=>
      (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 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)))