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

加法函數 (AdditionFn)

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

Ontology

SUMO / NUMERIC-FUNCTIONS

Class(es)

種類
is instance of
  可繼承關係  
is instance of
  二元函數  
is instance of
關連函數
is instance of
可換函數
is instance of
種類
is instance of
  可繼承關係  
is instance of
  與量關係  
is instance of
is instance of
  加法函數  

Coordinate term(s)

日函數  密度函數  除法函數  （文本）版本函數  指數函數  圖路徑函數  小時函數  交集函數  間隔函數  種類描述函數  列結函數  列序函數  對數函數  最大值函數  最大量路徑函數  測量函數  部分整體差異函數  部分整體交集函數  部分整體加總函數  最小值函數  最小量路徑函數  分鐘函數  月份函數  乘法函數  期刊一期函數  倒數函數  週期性時距函數  關係互補函數  相對時間函數  餘數函數  整數函數  秒鐘函數  系列一卷函數  速度函數  減法函數  時間單位函數  時間歷程函數  聯集函數  位置函數  相等  大於  大於或等於  小於  小於或等於 

Type restrictions

數量 AdditionFn(數量, 數量)

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 是 複數 的 實例, then there exist 實數 real1,實數 real2 so that number 等於 "(real1+"real2*" 的 平方根"")". 
(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?REAL1 ?REAL2)
            (and
                  (instance ?REAL1 RealNumber)
                  (instance ?REAL2 RealNumber)
                  (equal
                        ?NUMBER
                        (AdditionFn
                              ?REAL1
                              (MultiplicationFn
                                    ?REAL2
                                    (SquareRootFn -1)))))))
list3 等於 "list1 和 list2 組成的 序列" if and only if for all number1,number2 holds: if number1 小於或等於 "list1 的 長度" and number2 小於或等於 "list2 的 長度" and number1 是 正整數 的 實例 and number2 是 正整數 的 實例, then "list3 的 第二 元素" 等於 "list1 的 第二 元素" and "list3 的 第二 元素" 等於 "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))))))
(=>
      (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)" 等於 "(number+)". 
(equal
      (SuccessorFn ?NUMBER)
      (AdditionFn ?NUMBER 1))
"number1 取餘數 number2" 等於 number if and only if "(""最大 整數 小於 或 等於 "number1/number2""*number2"+number)" 等於 number1. 
(<=>
      (equal
            (RemainderFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (equal
            (AdditionFn
                  (MultiplicationFn
                        (FloorFn
                              (DivisionFn ?NUMBER1 ?NUMBER2))
                        ?NUMBER2)
                  ?NUMBER)
            ?NUMBER1))
是 加法函數 的 同�@元素. 
(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 "相對時間函數" 等於 time2, then time2 等於 "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 PacificTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 8)))
If "相對時間函數" 等於 time2, then time2 等於 "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 MountainTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 7)))
If "相對時間函數" 等於 time2, then time2 等於 "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 CentralTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 6)))
If "相對時間函數" 等於 time2, then time2 等於 "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 EasternTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 5)))