<p dir="ltr">Actually, change that m1-2 to m1-1 in the url</p>
<div class="gmail_quote">On Sep 10, 2013 10:17 AM, "Dr. ÉRDI Gergő" <<a href="mailto:gergo@erdi.hu">gergo@erdi.hu</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<p dir="ltr">Would this be of help? IIRC it uses an interface similar to the ring solver, but I can't check atm. <a href="http://perso.ens-lyon.fr/guillaume.allais/pdf/gallais_m1-2.pdf" target="_blank">http://perso.ens-lyon.fr/guillaume.allais/pdf/gallais_m1-2.pdf</a></p>
<div class="gmail_quote">On Sep 10, 2013 7:30 AM, "Rodrigo Ribeiro" <<a href="mailto:rodrigogribeiro@gmail.com" target="_blank">rodrigogribeiro@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr"><div><div><div>Hi!<br><br></div>I'm trying to prove the correctness of an algorithm and I'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>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div>
</blockquote></div>