Re: [isabelle] arith tactic



John,
The reasoning about mod in arith about mod and div is poor and enhancing it is on the TODO list. I recently wrote a more effitient implementation of the same QE algorithm, which is able to solve your problem whithin 3 minutes, running in ML (without proofs) which is just a pitty.

Presburger arithmetic is just too general to deal with mod and div in a practically acceptable manner. The decision problem in Presburger arithmetic is doubly exponential in space with respect to the largest constant occuring in the formula (255).

The bigger issue is that we'll be encountering many, many subgoals like this in our projects here, most of which involve reasoning about machine arithmetic. So we're relying on arith to discharge them automatically and efficiently.

Could you give me a "description" of this formula class?

Amine.





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