division fn (DivisionFn)

If number1 and number2 are Numbers, then (DivisionFn number1 number2) is the result of dividing number1 by number2. An exception occurs when number1 = 1, in which case (DivisionFn number1 number2) is the reciprocal of number2.

Ontologie

SUMO / NUMERIC-FUNCTIONS

Class(es)

třída

inheritable relation

binární funkce
is instance of

asociativní funkce
is instance of

třída

inheritable relation

relace rozšířená na veličiny
is instance of

division fn

Související termín(y)

addition fn day fn density 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 measure 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 reciprocal fn recurrent time interval fn relative complement fn relative time fn remainder fn round fn second fn series volume fn speed fn subtraction fn temporal composition fn time interval fn union fn where fn equal greater than greater than or equal to less than less than or equal to

Typy argumentů

veličina DivisionFn(veličina, veličina)

Related WordNet synsets

division: an arithmetic operation that is the inverse of multiplication; the quotient of two numbers is computed

See more related synsets on a separate page.

Axiomy (10)

Jestliže number je instancí třídy racionální číslo, potom existují celé číslo int1,celé číslo int2 tak, že number se rovná "int1/int2".

(=>
      (instance ?NUMBER RationalNumber)
      (exists
            (?INT1 ?INT2)
            (and
                  (instance ?INT1 Integer)
                  (instance ?INT2 Integer)
                  (equal
                        ?NUMBER
                        (DivisionFn ?INT1 ?INT2)))))

"number1 mod number2" se rovná number tehdy a jen tehdy pokud "(""floor fn(number1/number2)"*number2"+number)" se rovná number1.

(<=>
      (equal
            (RemainderFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (equal
            (AdditionFn
                  (MultiplicationFn
                        (FloorFn
                              (DivisionFn ?NUMBER1 ?NUMBER2))
                        ?NUMBER2)
                  ?NUMBER)
            ?NUMBER1))

Jestliže degree je instancí třídy jednotka plošného úhlu, potom "tangent fn(degree)" se rovná ""sine fn(degree)"/"cosine fn(degree)"".

(=>
      (instance ?DEGREE PlaneAngleMeasure)
      (equal
            (TangentFn ?DEGREE)
            (DivisionFn
                  (SineFn ?DEGREE)
                  (CosineFn ?DEGREE))))

je an identity element of division fn.

(identityElement DivisionFn 1)

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 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 angular degree(s)" se rovná ""number*"pi/"" radian(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER AngularDegree)
            (MeasureFn
                  (MultiplicationFn
                        ?NUMBER
                        (DivisionFn Pi 180))
                  Radian)))