Email Gateway (Aug 18 2022 at 12:57): Email Gateway (Aug 18 2022 at 12:57):From: Jens Doll <jd@cococo.de>
Isabelle now runs on my machine again and I thank Florian for helping me
with the installation. So I was able to enter some simple lemmata and to
rework my verification samples. (Excuse me for the buggy version
beforehand.) I added a third sample
http://cococo.de/products/windows/Columbo/sample3.html
which now contains a more difficult example: the function is rational and
multivariate, but the loop is linear in one variable.
Jens
P.S.: I still did not find the correct formula for the modular case,
sample2.html. Isabelle declines to solve the lemma. Does anyone know,
what's wrong there?
Email Gateway (Aug 18 2022 at 12:57):From: Tobias Nipkow <nipkow@in.tum.de>
The "lemma" on your web page
lemma sample2: "(EX j::nat.(ALL r::int.(r-2*j<=1)))"
is not even syntactically well-formed, has a type problem (nat/int) and
is definitely false. Your purported solution "j=2 dvd (r)" does not make
sense because your quantifiers are in the wrong order. If you swap them
and correct all the mistakes, it works:
lemma sample2: "ALL r::int. EX j. r - 2*j<=1"
by arith
Thanks to Amine.
Tobias
Email Gateway (Aug 18 2022 at 12:57):From: Amine Chaieb <ac638@cam.ac.uk>
Dear Jens,
I find it somehow difficult to isolate the problem (the formula) to be
proved. Could you send the formula? Is it over the integers or over the
reals?
If it is the latter, then there is a procedure that would eliminate you
the linear quantifiers. It is described in
[2] Amine Chaieb. Parametric Linear Arithmetic over Ordered Fields in
Isabelle/HOL. In Serge Autexier, John Campbell, Julio Rubio, Volker
Sorge, Masakazu Suzuki, and Freek Wiedijk, editors,
/AISC/MKM/Calculemus/, volume 5144 of /Lecture Notes in Computer
Science/, pages 246-260. Springer-Verlag, July 2008.
If it is over the integers though, then I only know of a procedure by
Weispfenning 1990, which has been reconsidered recently (2006 I think)
by Sturm. It might be implemented in REDLOG/REDUCE.
That theory does not admit quantifier elimination in the usual sense.
You need to introduce a new kind of quantifiers (not eliminated). I also
think it is not decidable.
Hope it helps,
Amine.
Jens Doll wrote:
Email Gateway (Aug 18 2022 at 12:57):From: Jens Doll <jd@cococo.de>
Thank you, Amine and Tobias,
the lemma sample2 has now been corrected. I also learned the term
"parametric linear arithmetic", which might be very useful for my work.
Maybe some day Columbo will output Isabelle theory files automatically ...
Jens
Email Gateway (Aug 18 2022 at 12:58):From: Tjark Weber <webertj@in.tum.de>
Jens,
I'm not sure what you're aiming to do exactly, but you might find the
"Why" tool (http://why.lri.fr/) interesting, and also Norbert Schirmer's
Ph.D. thesis (http://www4.in.tum.de/~schirmer/pub/schirmer-phd.html).
Regards,
Tjark
Last updated: May 03 2024 at 08:18 UTC