Re: [isabelle] Modular arithmetic theory?



> Does the Isabelle distribution contain efficient decision procedures  
> or a comprehensive simpset for linear arithmetic on numbers modulo a  
> fixed constant N, but where N can be large, such as 2^32?

I'm afraid not. Quantifier free linear arithmetic (which is reasonably
efficient) ignores mod completely. Presburger arithmetic (which is also
tried) deals with "mod n" where n is a numeral - but it appears far too slow
on these problems.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.