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"
 by arith

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

Cheers,
Amine





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