SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > Function > BinaryFunction > AssociativeFunction > SubtractionFn
Next AssociativeFunctionAdditionFn    UpAssociativeFunction, RelationExtendedToQuantities    Previous AssociativeFunctionMultiplicationFn   

SubtractionFndocumentation 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 ?NUMBER22001-11-30 13:35:22.0
has axiom
(equal (AbsoluteValueFn ?NUMBER1) ?NUMBER2)
(instance ?NUMBER1 PositiveInteger)
(equal ?NUMBER1 ?NUMBER2))
(instance ?NUMBER1 NegativeInteger)
(equal ?NUMBER2 (SubtractionFn 0 ?NUMBER1)))))
2001-11-30 13:35:22.0
has axiom
(equal (RoundFn ?NUMBER1) ?NUMBER2)
(lessThan (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5)
(equal ?NUMBER2 (FloorFn ?NUMBER1)))
(greaterThanOrEqualTo (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5)
(equal ?NUMBER2 (CeilingFn ?NUMBER1)))))
2001-11-30 13:35:22.0
has axiom
(MeasureFn ?NUMBER Celsius)
(MeasureFn (SubtractionFn ?NUMBER 273.15) Kelvin))
2001-11-30 13:35:22.0
has domain1 Quantity2001-11-30 13:35:22.0
has domain2 Quantity2001-11-30 13:35:22.0
has identityElement 02001-11-30 13:35:22.0
has range Quantity2001-11-30 13:35:22.0
is an instance of AssociativeFunction2001-11-30 13:35:22.0
is an instance of RelationExtendedToQuantities2001-11-30 13:35:22.0
BinaryFunctionis first domain of distributes2001-11-30 13:33:43.0
is first domain of identityElement2001-11-30 13:33:43.0
is second domain of distributes2001-11-30 13:33:43.0
Relationis first domain of domain2001-11-30 13:35:10.0
is first domain of domainSubclass2001-11-30 13:35:10.0
is first domain of holds2001-11-30 13:35:10.0
is first domain of subrelation2001-11-30 13:35:10.0
is first domain of valence2001-11-30 13:35:10.0
is second domain of subrelation2001-11-30 13:35:10.0
Classis third domain of domain2001-11-30 13:33:51.0
is third domain of domainSubclass2001-11-30 13:33:51.0
Abstractis disjoint from Physical2001-11-30 13:33:32.0

Next AssociativeFunctionAdditionFn    UpAssociativeFunction, RelationExtendedToQuantities    Previous AssociativeFunctionMultiplicationFn