Re: [isabelle] Modular arithmetic theory?



Hi,

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).

http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2004/root.pdf)
(see also a previous paper at:
http://kisogawa.inf.ethz.ch/WebBIB/publications-softech/papers/2003/0_fmics03.pdf)



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

Results:
========
-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

    http://arxiv.org/abs/cs.LO/0506008

 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 ...


Burkhart






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