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