Re: [isabelle] Integer Division
"Solving" such problems can be done using quantifier elimination. More
precisely with an extension called quantifier elimination with answers.
Quantifier elimination for this formula (which is in Presburger
arithmetic) just tells you that it is equivalent to "true". Quantifier
elimination with answers tells you it is equivalent to True and you that
one such an i is "(r - 1) div 2". These answers can be obtained from
e.g. Reddy and Loveland's algorithm (or any "equivalent", like
Weispfenning's 1990 etc...). These algorithms construct an "elimination
set" which contains all possible answers (i.e. if there is an i at all,
it must be one of them). From there you can find the answer.
If the problems are not very complicated (their logical structure) then
you might consider integer programming (there, however, everything
should be existentially quantified, i.e. r too in the example below).
The stength of QE with answers is that you can keep parameters in your
Jens Doll wrote:
thank you, that helped me a lot and I reconsidered the original problem. I
will have to teach my algorithm to solve the inequality
" EX (i::int). r - 2*i <= 1" ,
The final result could look like this
This archive was generated by a fusion of
Pipermail (Mailman edition) and