[Agda] Solving Presburger arithmetic goals

Dr. ÉRDI Gergő gergo at erdi.hu
Tue Sep 10 04:17:56 CEST 2013

Would this be of help? IIRC it uses an interface similar to the ring
solver, but I can't check atm.
On Sep 10, 2013 7:30 AM, "Rodrigo Ribeiro" <rodrigogribeiro at gmail.com>

> 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

More information about the Agda mailing list