Email Gateway (Aug 18 2022 at 12:44): Email Gateway (Aug 18 2022 at 12:44):From: Jens Doll <jd@cococo.de>
I have a little problem with the integer division. When solving the
equation
r-2*i=1
for integers i and r my algorithm gives
i=(1/2*r+r mod 2)-1/2,
which does not seem right.
Could someone tell me, how to calculate the result?
Thanks, Jens
Email Gateway (Aug 18 2022 at 12:45):From: Amine Chaieb <ac638@cam.ac.uk>
Dear Jens,
A test with presburger will show that such an i does not always exist:
lemma " EX (i::int). r - 2i = 1" apply presburger ( Fails *)
There was a feature on how to get an equivalent formula for that (now
only available from ML). You can let Isabelle prove automatically for you:
"(EX (i::int). r - 2*i = 1) == 2 dvd (r - 1)"
which means that such an i exists if and only if r is odd. From there
it is easy to define a solution.
Hope it helps,
Amine.
Jens Doll wrote:
Email Gateway (Aug 18 2022 at 12:45):From: Jens Doll <jd@cococo.de>
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
http://cococo.de/products/windows/Columbo/sample2.html
Regards,
Jens
Email Gateway (Aug 18 2022 at 12:46):From: Amine Chaieb <ac638@cam.ac.uk>
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,
Amine.
Jens Doll wrote:
Email Gateway (Aug 18 2022 at 12:46):From: Tjark Weber <webertj@in.tum.de>
Jens,
this (again) falls within the scope of Presburger arithmetic, and is
handled automatically by Isabelle:
lemma "EX (i::int). r - 2*i <= 1"
by presburger
Regards,
Tjark
Last updated: May 03 2024 at 04:19 UTC