 SUMO   View all facts   Glossary   Help Entity > Abstract > Class > Relation > Function > BinaryFunction > AssociativeFunction > SubtractionFn
Next AssociativeFunctionAdditionFn    UpAssociativeFunction, RelationExtendedToQuantities    Previous AssociativeFunctionMultiplicationFn  SubtractionFn subject fact
 SubtractionFn documentation 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 has axiom `(<=> (equal (AbsoluteValueFn ?NUMBER1) ?NUMBER2) (or (and (instance ?NUMBER1 PositiveInteger) (equal ?NUMBER1 ?NUMBER2)) (and (instance ?NUMBER1 NegativeInteger) (equal ?NUMBER2 (SubtractionFn 0 ?NUMBER1)))))` has axiom `(=> (equal (RoundFn ?NUMBER1) ?NUMBER2) (or (=> (lessThan (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (FloorFn ?NUMBER1))) (=> (greaterThanOrEqualTo (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (CeilingFn ?NUMBER1)))))` has axiom `(equal (MeasureFn ?NUMBER Celsius) (MeasureFn (SubtractionFn ?NUMBER 273.15) Kelvin))` has domain1 Quantity has domain2 Quantity has identityElement 0 has range Quantity is an instance of AssociativeFunction is an instance of RelationExtendedToQuantities BinaryFunction is first domain of distributes is first domain of identityElement is second domain of distributes Relation is first domain of domain is first domain of domainSubclass is first domain of holds is first domain of subrelation is first domain of valence is second domain of subrelation Class is third domain of domain is third domain of domainSubclass Abstract is disjoint from Physical  Next AssociativeFunctionAdditionFn    UpAssociativeFunction, RelationExtendedToQuantities    Previous AssociativeFunctionMultiplicationFn