nezáporné reálné číslo (NonnegativeRealNumber)

A RealNumber that is greater than or equal to zero.

Ontologie

SUMO / BASE-ONTOLOGY

Nadtřída(y)

entita

abstraktum

veličina

číslo

reálné číslo

nezáporné reálné číslo

Podtřída(y)

kladné reálné číslo nezáporné celé číslo

Související termín(y)

binární číslo iracionální číslo záporné reálné číslo racionální číslo

Constrains relations

absolute value fn

Related WordNet synsets

nonnegative: (mathematics) either positive or zero

Axiomy (4)

reálné číslo je exhaustively partitioned into záporné reálné číslo,nezáporné reálné číslo.

(partition RealNumber NegativeRealNumber NonnegativeRealNumber)

number je instancí třídy nezáporné reálné číslo tehdy a jen tehdy pokud number je větší než nebo roven a number je instancí třídy reálné číslo.

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

"absolute value fn(number1)" se rovná number2 a number1 je instancí třídy reálné číslo a number2 je instancí třídy reálné číslo tehdy a jen tehdy pokud

number1 je instancí třídy nezáporné reálné číslo a number1 se rovná number2
number1 je instancí třídy záporné reálné číslo a number2 se rovná "(-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)))))

Jestliže number je instancí třídy nezáporné reálné číslo, potom "signum fn(number)" se rovná nebo "signum fn(number)" se rovná .

(=>
      (instance ?NUMBER NonnegativeRealNumber)
      (or
            (equal
                  (SignumFn ?NUMBER)
                  1)
            (equal
                  (SignumFn ?NUMBER)
                  0)))