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