SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > Function > BinaryFunction > AssociativeFunction > AdditionFn
Next AssociativeFunctionDivisionFn    UpAssociativeFunction, CommutativeFunction, RelationExtendedToQuantities    Previous AssociativeFunctionSubtractionFn   

AdditionFn
subjectfact 
AdditionFndocumentation If ?NUMBER1 and ?NUMBER2 are Numbers, then (AdditionFn ?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers2001-11-30 13:33:32.0
has axiom
(<=>
(equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
(equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
2001-11-30 13:33:32.0
has domain1 Quantity2001-11-30 13:33:32.0
has domain2 Quantity2001-11-30 13:33:32.0
has identityElement 02001-11-30 13:33:32.0
has range Quantity2001-11-30 13:33:32.0
is an instance of AssociativeFunction2001-11-30 13:33:33.0
is an instance of CommutativeFunction2001-11-30 13:33:33.0
is an instance of RelationExtendedToQuantities2001-11-30 13:33:33.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 AssociativeFunctionDivisionFn    UpAssociativeFunction, CommutativeFunction, RelationExtendedToQuantities    Previous AssociativeFunctionSubtractionFn