Re: [isabelle] arith tactic
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
Could you give me a "description" of this formula class?
This archive was generated by a fusion of
Pipermail (Mailman edition) and