[Agda] Solving Presburger arithmetic goals

Rodrigo Ribeiro rodrigogribeiro at gmail.com
Tue Sep 10 01:30:06 CEST 2013


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130909/af978e11/attachment.html

More information about the Agda mailing list