[Agda] Solving Presburger arithmetic goals

[Dr. ÉRDI Gergő]

Actually, change that m1-2 to m1-1 in the url
On Sep 10, 2013 10:17 AM, "Dr. ÉRDI Gergő" <gergo at erdi.hu> wrote:

> 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/1abda7ca/attachment.html