Zvolte jazyk: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi
Koncept:
Anglické slovo:
Hlavní stránka

addition fn (AdditionFn)

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

Ontologie

SUMO / NUMERIC-FUNCTIONS

Class(es)

třída
is instance of
  inheritable relation  
is instance of
  binární funkce  
is instance of
asociativní funkce
is instance of
komutativní funkce
is instance of
třída
is instance of
  inheritable relation  
is instance of
  relace rozšířená na veličiny  
is instance of
is instance of
  addition fn  

Související termín(y)

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 

Typy argumentů

veličina AdditionFn(veličina, veličina)

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.

Axiomy (12)

Jestliže number je instancí třídy komplexní číslo, potom existují reálné číslo real1,reálné číslo real2 tak, že number se rovná "(real1+"real2*"square root fn()"")". 
(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?REAL1 ?REAL2)
            (and
                  (instance ?REAL1 RealNumber)
                  (instance ?REAL2 RealNumber)
                  (equal
                        ?NUMBER
                        (AdditionFn
                              ?REAL1
                              (MultiplicationFn
                                    ?REAL2
                                    (SquareRootFn -1)))))))
list3 se rovná "list concatenate fn(list1,list2)" tehdy a jen tehdy pokud pro všechny number1,number2 platí: jestliže number1 je menší než nebo roven "length of list1" a number2 je menší než nebo roven "length of list2" a number1 je instancí třídy kladné celé číslo a number2 je instancí třídy kladné celé číslo, potom "number1th element of list3" se rovná "number1th element of list1" a ""("length of list1"+number2)"th element of list3" se rovná "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))))))
(=>
      (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)" se rovná "(number+)". 
(equal
      (SuccessorFn ?NUMBER)
      (AdditionFn ?NUMBER 1))
"number1 mod number2" se rovná number tehdy a jen tehdy pokud "(""floor fn(number1/number2)"*number2"+number)" se rovná number1. 
(<=>
      (equal
            (RemainderFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (equal
            (AdditionFn
                  (MultiplicationFn
                        (FloorFn
                              (DivisionFn ?NUMBER1 ?NUMBER2))
                        ?NUMBER2)
                  ?NUMBER)
            ?NUMBER1))
je an identity element of addition fn. 
(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)))
Jestliže "relative time fn(time1,pacific time zone)" se rovná time2, potom time2 se rovná "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 PacificTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 8)))
Jestliže "relative time fn(time1,mountain time zone)" se rovná time2, potom time2 se rovná "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 MountainTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 7)))
Jestliže "relative time fn(time1,central time zone)" se rovná time2, potom time2 se rovná "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 CentralTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 6)))
Jestliže "relative time fn(time1,eastern time zone)" se rovná time2, potom time2 se rovná "(time1+)". 
(=>
      (equal
            (RelativeTimeFn ?TIME1 EasternTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 5)))