Email Gateway (Aug 18 2022 at 13:00): Email Gateway (Aug 18 2022 at 13:00):From: Dominik Luecke <luecke@informatik.uni-bremen.de>
Hello,
Lutz Schroeder asked a very similar similar question on 19 Oct 2007, I
am adding the reference here:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2007-October/msg00028.html
Currently I am working on a proof in Isabelle needs a lot of arithmetic
reasoning, that Isabelle cannot handle on its own. Is there an recent
and working (best compatible with Isabelle version 2008) interface from
Isabelle to a computer algebra system? As Lutz already mentioned
searching the web for "Isabelle" and "Computer Algebra" only reveals
papers on a very old interface (pre-2003).
My second question is regarding large proof goals, in fact large sets of
assumptions. Currently Isabelle is not able to find contradictions like
[|...; x < 0; ...; 0 < x; ... |] ==> 1 = -1 in this set of assumptions,
and I need to derive these contradictions basically by hand. I never
counted them completely, but I seem to have about 150 assumptions.
Regards,
Dominik
Email Gateway (Aug 18 2022 at 13:02):From: Tjark Weber <webertj@in.tum.de>
Dominik,
I'm surprised this is not handled by 'arith', regardless of the number
of assumptions. If your question is still open, feel free to send me an
example theory where the problem occurs.
Regards,
Tjark
Last updated: May 03 2024 at 12:27 UTC