most recent 30 from http://mathoverflow.net 2013-05-21T19:03:49Z http://mathoverflow.net/feeds/user/11052 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/31270/complete-mathematics/47186#47186 anon 2010-11-24T03:05:45Z 2010-11-24T03:05:45Z

<p>Presberger arithmetic is used in practice for software verification, e.g. to prove that a program fragment is free of array subscript overflows. Basically the program has expressions like a[3*i+k] and you want to prove that the subscript never greater than the array size. If you have something like a[m*n+k] the multiplication of two variables m and n can only be expressed in Peano arithmetic, which is undecidable, but it's often possible to write programs without such multiplications of variables in subscripts. (Multiplication by constants can be expressed by repeated addition, of course). Wikipedia's article on Presburger arithmetic has some info of that.</p> <p>Also, compilers of fancy programming languages rely on decidability of even weaker theories to handle type inference and type equality. Similarly for model checking in hardware design, etc. This stuff is becoming more and more important in the real world, and not that many programmers and engineers know much about it. I think this is a good time to be a logician even if you can't get a job in academia.</p>