Re: [isabelle] Modular arithmetic theory?


I made an Isabelle theory on 2's complement
arithmetic (for Isabelle 2003) together with 
Javas Specification of mod and div.

Nicole Rauch and Burkhart Wolff. Formalizing Java's Two's-Complement
Integral Type in Isabelle/HOL. ETH Zürich, Technical Report 458, 2004.
(abstract) (BibTeX entry) (PDF).
(see also a previous paper at:

At that time, we also investigated the possibility
of decision procedures for such type of arithmetic.

-An attempt to decide a challenge problem

   "(x div y) * y + (x mod y) = x"

 (div, mod, + * all 2's complement operations,
  such a property is required for the integers
  in the Java Language Specification)

 with an up-to-date wordlevel-BDD package
 was only feasible for a bit-length of 5 (!).

-A "translation-approach" (compile away 2's complement 
 div mod * + into ones on standard int) leads to
 a linear growth of the number of modulos (and difference 
 operations); roughly speaking, worst case complexity bounds 
 for automata-based PA decision procedure depend on this 
 number exponentially, see Felix Klaedtkes Work "Bounds on 
 the Automata Size for Presburger Arithmetic", Theorem 4.5, 
 pp. 23, see

 for details.

 Klaedtke also estimates that symbolic procedures
 like Coopers Algorithm will behave similarly.

-I'm still interested how a modern SAT solver like
 chaff behaves for the challenge problem above;
 so far, I failed to interest people from the
 SAT community ... At least, I never learnt 
 anything about their results ...


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