addition fn (AdditionFn)
If number1 and number2 are Numbers, then
(AdditionFn number1 number2) is the arithmetical sum of these
numbers.
Ontology
SUMO / NUMERIC-FUNCTIONSClass(es)
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
Type restrictions
quantity AdditionFn(quantity, quantity)
Related WordNet synsets
- summation, addition, plus
- 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
(AdditionFn
?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
(AdditionFn
(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
(AdditionFn ?NUMBER1 ?NUMBER3))))))))
"(number+1)" is equal to "(number+)".
(equal
(SuccessorFn ?NUMBER)
(AdditionFn ?NUMBER 1))
"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
(AdditionFn
(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
(AdditionFn
(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)
(AdditionFn ?NUMBER1 ?NUMBER2)))
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
(AdditionFn ?TIME1 8)))
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
(AdditionFn ?TIME1 7)))
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
(AdditionFn ?TIME1 6)))
If "relative time fn(time1,eastern time zone)" is equal to time2, then time2 is equal to "(time1+)".
(=>
(equal
(RelativeTimeFn ?TIME1 EasternTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 5)))
