[Agda] Solving Presburger arithmetic goals

[Dr. ÉRDI Gergő]

Would this be of help? IIRC it uses an interface similar to the ring
solver, but I can't check atm.
http://perso.ens-lyon.fr/guillaume.allais/pdf/gallais_m1-2.pdf
On Sep 10, 2013 7:30 AM, "Rodrigo Ribeiro" <rodrigogribeiro at gmail.com>
wrote:

> Hi!
>
> 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.
>
> I noticed that the Standard library has solvers for semi-rings. Is there
> some solver for Presburger arithmetic ?
>
> -- Rodrigo
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130910/eb0a097b/attachment.html