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

If number1 and number2 are Numbers, then (AdditionFn number1 number2) is the arithmetical sum of these numbers.

## Ontology

SUMO / NUMERIC-FUNCTIONS

## Class(es)

 class

inheritable relation

binary function
 associative function
 commutative function
 class

inheritable relation

relation extended to quantities

## Coordinate term(s)

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  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

## Related WordNet synsets

the arithmetic operation of summing; calculating the sum of two or more numbers; "the summation of four and three gives seven"; "four plus three equals seven"

See more related synsets on a separate page.

## Axioms (12)

If number is an instance of complex number, then there exist real number real1,real number real2 so that number is equal to "(real1+"real2*"the square root of "")".
```(=>
(instance ?NUMBER ComplexNumber)
(exists
(?REAL1 ?REAL2)
(and
(instance ?REAL1 RealNumber)
(instance ?REAL2 RealNumber)
(equal
?NUMBER
?REAL1
(MultiplicationFn
?REAL2
(SquareRootFn -1)))))))```

list3 is equal to "the list composed of list1 and list2" if and only if for all number1,number2 holds: if number1 is less than or equal to "length of list1" and number2 is less than or equal to "length of list2" and number1 is an instance of positive integer and number2 is an instance of positive integer, then "number1th element of list3" is equal to "number1th element of list1" and ""("length of list1"+number2)"th element of list3" is equal to "number2th element of list2".
```(<=>
(equal
?LIST3
(ListConcatenateFn ?LIST1 ?LIST2))
(forall
(?NUMBER1 ?NUMBER2)
(=>
(and
(lessThanOrEqualTo
?NUMBER1
(ListLengthFn ?LIST1))
(lessThanOrEqualTo
?NUMBER2
(ListLengthFn ?LIST2))
(instance ?NUMBER1 PositiveInteger)
(instance ?NUMBER2 PositiveInteger))
(and
(equal
(ListOrderFn ?LIST3 ?NUMBER1)
(ListOrderFn ?LIST1 ?NUMBER1))
(equal
(ListOrderFn
?LIST3
(ListLengthFn ?LIST1)
?NUMBER2))
(ListOrderFn ?LIST2 ?NUMBER2))))))```

• if list1 is a sublist of list2,
• then there exists number3 so that for all item holds: if item is a member of list1, then there exist number1,number2 so that "number1th element of list1" is equal to item and "number2th element of list2" is equal to item and number2 is equal to "(number1+number3)"
• .
```(=>
(subList ?LIST1 ?LIST2)
(exists
(?NUMBER3)
(forall
(?ITEM)
(=>
(inList ?ITEM ?LIST1)
(exists
(?NUMBER1 ?NUMBER2)
(and
(equal
(ListOrderFn ?LIST1 ?NUMBER1)
?ITEM)
(equal
(ListOrderFn ?LIST2 ?NUMBER2)
?ITEM)
(equal
?NUMBER2

"(number+1)" is equal to "(number+)".
```(equal
(SuccessorFn ?NUMBER)

"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
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2))
?NUMBER2)
?NUMBER)
?NUMBER1))```

is an identity element of addition fn.
`(identityElement AdditionFn 0)`

• if
• "the value of path" is equal to sum
• and
• subpath is a subgraph of path
• and
• arc1 is a part of path
• and
• the value of arc1 is number1
• and
• for all arc2 holds: if arc2 is a part of path, then arc2 is a part of subpath or arc2 is equal to arc1
,
• then sum is equal to "("the value of subpath"+number1)"
• .
```(=>
(and
(equal
(PathWeightFn ?PATH)
?SUM)
(subGraph ?SUBPATH ?PATH)
(graphPart ?ARC1 ?PATH)
(arcWeight ?ARC1 ?NUMBER1)
(forall
(?ARC2)
(=>
(graphPart ?ARC2 ?PATH)
(or
(graphPart ?ARC2 ?SUBPATH)
(equal ?ARC2 ?ARC1)))))
(equal
?SUM
(PathWeightFn ?SUBPATH)
?NUMBER1)))```

• if
• "the value of path" is equal to sum
• and
• arc1 is a part of path
• and
• arc2 is a part of path
• and
• the value of arc1 is number1
• and
• the value of arc2 is number2
• and
• for all arc3 holds: if arc3 is a part of path, then arc3 is equal to arc1 or arc3 is equal to arc2
,
• then "the value of path" is equal to "(number1+number2)"
• .
```(=>
(and
(equal
(PathWeightFn ?PATH)
?SUM)
(graphPart ?ARC1 ?PATH)
(graphPart ?ARC2 ?PATH)
(arcWeight ?ARC1 ?NUMBER1)
(arcWeight ?ARC2 ?NUMBER2)
(forall
(?ARC3)
(=>
(graphPart ?ARC3 ?PATH)
(or
(equal ?ARC3 ?ARC1)
(equal ?ARC3 ?ARC2)))))
(equal
(PathWeightFn ?PATH)

If "relative time fn(time1,pacific time zone)" is equal to time2, then time2 is equal to "(time1+)".
```(=>
(equal
(RelativeTimeFn ?TIME1 PacificTimeZone)
?TIME2)
(equal
?TIME2

If "relative time fn(time1,mountain time zone)" is equal to time2, then time2 is equal to "(time1+)".
```(=>
(equal
(RelativeTimeFn ?TIME1 MountainTimeZone)
?TIME2)
(equal
?TIME2

If "relative time fn(time1,central time zone)" is equal to time2, then time2 is equal to "(time1+)".
```(=>
(equal
(RelativeTimeFn ?TIME1 CentralTimeZone)
?TIME2)
(equal
?TIME2
```(=>