<div dir="ltr"><div><div><div>Hi!<br><br></div>I&#39;m trying to prove the correctness of an algorithm and I&#39;m facing some boring proofs that could be easily proved (in Coq, at least...) by a decision procedure for the Presburger arithmetic.<br>
<br></div>I noticed that the Standard library has solvers for semi-rings. Is there some solver for Presburger arithmetic ?<br><br></div>-- Rodrigo<br></div>