[Agda] Solving Presburger arithmetic goals
Dr. ÉRDI Gergő
gergo at erdi.hu
Tue Sep 10 04:20:14 CEST 2013
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.
> On Sep 10, 2013 7:30 AM, "Rodrigo Ribeiro" <rodrigogribeiro at gmail.com>
>> 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda