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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and