[Agda] Solving Presburger arithmetic goals
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 ?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda