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