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

subtraction fn (SubtractionFn)

If number1 and number2 are Numbers, then (SubtractionFn number1 number2) is the arithmetical difference between number1 and number2, i.e. number1 minus number2. An exception occurs when number1 is equal to 0, in which case (SubtractionFn number1 number2) is the negation of number2.

Ontology

SUMO / NUMERIC-FUNCTIONS

Class(es)

class
is instance of
  inheritable relation  
is instance of
  binary function  
is instance of
associative function
is instance of
class
is instance of
  inheritable relation  
is instance of
  relation extended to quantities  
is instance of
is instance of
  subtraction fn  

Coordinate term(s)

addition fn  day fn  density fn  division 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  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 SubtractionFn(quantity, quantity)

Related WordNet synsets

subtraction, minus
an arithmetic operation in which the difference between two numbers is calculated; "the subtraction of three from four leaves one"; "four minus three equals one"
subtraction is kind of (all)...   subtraction is kind of...  
See more related synsets on a separate page.

Axioms (11)

"(number+2)" is equal to "(number-)". 
(equal
      (PredecessorFn ?NUMBER)
      (SubtractionFn ?NUMBER 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 
(<=>
      (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)))))
(=>
      (equal
            (RoundFn ?NUMBER1)
            ?NUMBER2)
      (or
            (=>
                  (lessThan
                        (SubtractionFn
                              ?NUMBER1
                              (FloorFn ?NUMBER1))
                        0.5)
                  (equal
                        ?NUMBER2
                        (FloorFn ?NUMBER1)))
            (=>
                  (greaterThanOrEqualTo
                        (SubtractionFn
                              ?NUMBER1
                              (FloorFn ?NUMBER1))
                        0.5)
                  (equal
                        ?NUMBER2
                        (CeilingFn ?NUMBER1)))))
is an identity element of subtraction fn. 
(identityElement SubtractionFn 0)
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 day1 is an instance of "the day number1" and day2 is an instance of "the day number2" and "(number2-number1)" is equal to , then day1 meets day2. 
(=>
      (and
            (instance
                  ?DAY1
                  (DayFn ?NUMBER1 ?MONTH))
            (instance
                  ?DAY2
                  (DayFn ?NUMBER2 ?MONTH))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?DAY1 ?DAY2))
If hour1 is an instance of "the hour number1" and hour2 is an instance of "the hour number2" and "(number2-number1)" is equal to , then hour1 meets hour2. 
(=>
      (and
            (instance
                  ?HOUR1
                  (HourFn ?NUMBER1 ?DAY))
            (instance
                  ?HOUR2
                  (HourFn ?NUMBER2 ?DAY))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?HOUR1 ?HOUR2))
If minute1 is an instance of "the minute number1" and minute2 is an instance of "the minute number2" and "(number2-number1)" is equal to , then minute1 meets minute2. 
(=>
      (and
            (instance
                  ?MINUTE1
                  (MinuteFn ?NUMBER1 ?HOUR))
            (instance
                  ?MINUTE2
                  (MinuteFn ?NUMBER2 ?HOUR))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?MINUTE1 ?MINUTE2))
If second1 is an instance of "the second number1" and second2 is an instance of "the second number2" and "(number2-number1)" is equal to , then second1 meets second2. 
(=>
      (and
            (instance
                  ?SECOND1
                  (SecondFn ?NUMBER1 ?MINUTE))
            (instance
                  ?SECOND2
                  (SecondFn ?NUMBER2 ?MINUTE))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?SECOND1 ?SECOND2))
If year1 is an instance of year and year2 is an instance of year and "(year2-year1)" is equal to , then year1 meets year2. 
(=>
      (and
            (instance ?YEAR1 Year)
            (instance ?YEAR2 Year)
            (equal
                  (SubtractionFn ?YEAR2 ?YEAR1)
                  1))
      (meetsTemporally ?YEAR1 ?YEAR2))