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.

Ontology

SUMO / NUMERIC-FUNCTIONS

Class(es)

class

inheritable relation

binary function
is instance of

associative function
is instance of

class

inheritable relation

relation extended to quantities
is instance of

division fn

Coordinate term(s)

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

Type restrictions

quantity DivisionFn(quantity, quantity)

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.

Axioms (10)

If number is an instance of rational number, then there exist integer int1,integer int2 so that number is equal to "int1/int2".

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

"number1 mod number2" is equal to number if and only if "(""the largest integer less than or equal to "number1/number2""*number2"+number)" is equal to number1.

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

If degree is an instance of plane angle measure, then "the tangent of degree" is equal to ""the sine of degree"/"the cosine of degree"".

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

is an identity element of division fn.

(identityElement DivisionFn 1)

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 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 angular degree(s)" is equal to ""number*"pi/"" radian(s)".

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