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

nonnegative real number (NonnegativeRealNumber)

A RealNumber that is greater than or equal to zero.

Ontology

SUMO / BASE-ONTOLOGY

Superclass(es)

[tree]
entity
is subclass of
  abstract  
is subclass of
  quantity  
is subclass of
  number  
is subclass of
  real number  
is subclass of
  nonnegative real number  

Subclass(es)

positive real number  nonnegative integer 

Coordinate term(s)

binary number  irrational number  negative real number  rational number 

Constrains relations

absolute value fn 

Related WordNet synsets

nonnegative
(mathematics) either positive or zero
nonnegative is similar to...  

Axioms (4)

real number is exhaustively partitioned into negative real number,nonnegative real number. 
(partition RealNumber NegativeRealNumber NonnegativeRealNumber)
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)))
"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 
(<=>
      (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 number is an instance of nonnegative real number, then "the sign of number" is equal to or "the sign of number" is equal to . 
(=>
      (instance ?NUMBER NonnegativeRealNumber)
      (or
            (equal
                  (SignumFn ?NUMBER)
                  1)
            (equal
                  (SignumFn ?NUMBER)
                  0)))