Arithmetic Addition Operation

From GM-RKB
(Redirected from Sum)
Jump to: navigation, search

An Arithmetic Addition Operation is an binary arithmetic operation that continues the count of each input.



References

2011

2009

  • http://www.isi.edu/~hobbs/bgt-arithmetic.text
    • We will define addition recursively in terms of the "successor" relation. The predication "(sum n1 n2 n3)" means that n1 is the sum of [math]n_2[/math] and [math]n_3[/math]. The sum of a number [math]n[/math] and zero is [math]n[/math]. (8) (forall (n) (sum n n 0))
    • The recursive step is as follows: (9) (forall (n n1 n2 n3 n4) (if (and (successor n3 n2)(sum n4 n1 n2)) (iff (sum n n1 n3)(successor n n4))))
    • The more conventional and more succinct way of saying this is "[math]n_1+S(n_2) = S(n_1+n_2)[/math]".