Presburger Arithmetic Decision Procedures
John Harrison's handbook on automated theorem proving contains a fairly detailed description of Cooper's algorithm, including the steps necessary for an implementation in ML.

Harrison, J. (2009). Handbook of practical logic and automated reasoning. Cambridge University Press.