Re: [isabelle] Integer Division

Dear Jens,

"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 (existential) problem.

Best wishes,

Jens Doll wrote:
Hello Amine,

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 MHonArc.