*To*: matthews at galois.com*Subject*: Re: [isabelle] Modular arithmetic theory?*From*: nipkow at in.tum.de*Date*: Thu, 10 Nov 2005 05:30:29 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <2034DB73-17B2-4337-B25B-047C9328BF87@galois.com> (message from John Matthews on Wed, 9 Nov 2005 15:28:36 -0800)*References*: <2034DB73-17B2-4337-B25B-047C9328BF87@galois.com>

> 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

**Follow-Ups**:**Re: [isabelle] Modular arithmetic theory?***From:*Amine Chaieb

**References**:**[isabelle] Modular arithmetic theory?***From:*John Matthews

- Previous by Date: Re: [isabelle] Modular arithmetic theory?
- Next by Date: Re: [isabelle] Modular arithmetic theory?
- Previous by Thread: Re: [isabelle] Modular arithmetic theory?
- Next by Thread: Re: [isabelle] Modular arithmetic theory?
- Cl-isabelle-users November 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list