Re: [isabelle] Modular arithmetic theory?
The problem with arith in the original problem
lemma "(n mod 4294967296 + m mod 4294967296) mod 4294967296 = (m + n) mod 4294967296"
is a bit different from what i first thought. In fact, the code for
presburger arithmetic is never called, not even the preparation step i was
talking about in previous mail.
Thanks Michael for the discussion, i now enhanced the preparation step and
can prove the theorem above in 0.020 seconds. Altough please use
temporarily "presburger" and not arith. Hopefully the arith problem will
be solved soon.
A propos the split rule with the "4" universal quantifiers: If k is a
numeral in m mod k (which is neceesary for our implementation of
presburger, we don't consider uniform presburger arithmetic), and you add
computation rules for numerals then at
least one of the two quantifier blocks will vanish and most two remain
at the end.
On Thu, 17 Nov 2005, Michael Norrish
Even with so-called "delta-elimination" enabled, I can't get
comparable performance out of Cooper's algorithm, which is a shame.
I don't see why this is specific to cooper and not Omega test.
This archive was generated by a fusion of
Pipermail (Mailman edition) and