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

jia1 fa3 han2 shu4 (AdditionFn)

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

Ontology

SUMO / NUMERIC-FUNCTIONS

Class(es)

zhong3 lei4
is instance of
  ke3 ji4 cheng2 guan1 xi4  
is instance of
  er4 yuan2 han2 shu4  
is instance of
guan1 lian2 han2 shu4
is instance of
ke3 huan4 han2 shu4
is instance of
zhong3 lei4
is instance of
  ke3 ji4 cheng2 guan1 xi4  
is instance of
  yu3 liang4 guan1 xi4  
is instance of
is instance of
  jia1 fa3 han2 shu4  

Coordinate term(s)

ri4 han2 shu4  mi4 du4 han2 shu4  chu2 fa3 han2 shu4  wen2 ben3 ban3 ben3 han2 shu4  zhi3 shu4 han2 shu4  tu2 lu4 jing4 han2 shu4  xiao3 shi2 han2 shu4  jiao1 ji2 han2 shu4  jian1 ge2 han2 shu4  zhong3 lei4 miao2 shu4 han2 shu4  lie4 jie2 han2 shu4  lie4 xu4 han2 shu4  dui4 shu4 han2 shu4  zui4 da4 zhi2 han2 shu4  zui4 da4 liang4 lu4 jing4 han2 shu4  ce4 liang4 han2 shu4  bu4 fen5 zheng3 ti1 cha4 yi4 han2 shu4  bu4 fen5 zheng3 ti1 jiao1 ji2 han2 shu4  bu4 fen5 zheng3 ti1 jia1 zong1 han2 shu4  zui4 xiao3 zhi2 han2 shu4  zui4 xiao3 liang4 lu4 jing4 han2 shu4  fen1 zhong1 han2 shu4  yue4 fen4 han2 shu4  cheng2 fa3 han2 shu4  qi1 kan1 yi1 qi1 han2 shu4  dao3 shu4 han2 shu4  zhou1 qi1 xing4 shi2 ju4 han2 shu4  guan1 xi4 hu4 bu3 han2 shu4  xiang4 dui4 shi2 jian1 han2 shu4  yu2 shu4 han2 shu4  zheng3 shu4 han2 shu4  miao3 zhong1 han2 shu4  xi4 lie4 yi1 juan4 han2 shu4  su4 du4 han2 shu4  jian3 fa3 han2 shu4  shi2 jian1 dan1 wei4 han2 shu4  shi2 jian1 li4 cheng2 han2 shu4  lian2 ji2 han2 shu4  wei4 zhi4 han2 shu4  xiang1 deng3  da4 yu1  da4 yu1 huo4 deng3 yu1  xiao3 yu1  xiao3 yu1 huo4 deng3 yu1 

Type restrictions

shu4 liang4 AdditionFn(shu4 liang4, shu4 liang4)

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"
summation is kind of (all)...   summation is kind of...  
See more related synsets on a separate page.

Axioms (12)

If number shi4 fu4 shu4 de5 shi2 li4, then there exist shi2 shu4 real1,shi2 shu4 real2 so_that_not number deng3 yu1 "(real1+"real2*" de5 ping2 fang1 gen1"")". 
(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?REAL1 ?REAL2)
            (and
                  (instance ?REAL1 RealNumber)
                  (instance ?REAL2 RealNumber)
                  (equal
                        ?NUMBER
                        (AdditionFn
                              ?REAL1
                              (MultiplicationFn
                                    ?REAL2
                                    (SquareRootFn -1)))))))
list3 deng3 yu1 "list1 he2 list2 zu3 cheng2 de5 xu4 lie4" if and only if for all number1,number2 holds: if number1 小於或等於 "list1 de5 chang2 du4" and number2 小於或等於 "list2 de5 chang2 du4" and number1 shi4 zheng4 zheng3 shu4 de5 shi2 li4 and number2 shi4 zheng4 zheng3 shu4 de5 shi2 li4, then "list3 de5 di4 er4 yuan2 su4" deng3 yu1 "list1 de5 di4 er4 yuan2 su4" and "list3 de5 di4 er4 yuan2 su4" deng3 yu1 "list2 de5 di4 er4 yuan2 su4". 
(<=>
      (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))))))
(=>
      (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)" deng3 yu1 "(number+)". 
(equal
      (SuccessorFn ?NUMBER)
      (AdditionFn ?NUMBER 1))
"number1 qu3 yu2 shu4 number2" deng3 yu1 number if and only if "(""zui4 da4 zheng3 shu4 xiao3 yu1 huo4 deng3 yu1 "number1/number2""*number2"+number)" deng3 yu1 number1. 
(<=>
      (equal
            (RemainderFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (equal
            (AdditionFn
                  (MultiplicationFn
                        (FloorFn
                              (DivisionFn ?NUMBER1 ?NUMBER2))
                        ?NUMBER2)
                  ?NUMBER)
            ?NUMBER1))
shi4 jia1 fa3 han2 shu4 de5 tong2 yi1 yuan2 su4. 
(identityElement AdditionFn 0)
(=>
      (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)))
(=>
      (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 "xiang4 dui4 shi2 jian1 han2 shu4" deng3 yu1 time2, then time2 deng3 yu1 "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 PacificTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 8)))
If "xiang4 dui4 shi2 jian1 han2 shu4" deng3 yu1 time2, then time2 deng3 yu1 "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 MountainTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 7)))
If "xiang4 dui4 shi2 jian1 han2 shu4" deng3 yu1 time2, then time2 deng3 yu1 "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 CentralTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 6)))
If "xiang4 dui4 shi2 jian1 han2 shu4" deng3 yu1 time2, then time2 deng3 yu1 "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 EasternTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 5)))