Arithmetic Addition Operation

From GM-RKB
Jump to navigation Jump to 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]\displaystyle{ n_2 }[/math] and [math]\displaystyle{ n_3 }[/math]. The sum of a number [math]\displaystyle{ n }[/math] and zero is [math]\displaystyle{ 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]\displaystyle{ n_1+S(n_2) = S(n_1+n_2) }[/math]".