# [isabelle] Isabelle and Computer Algebra (revisted) / Large Proof Goals

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
--
Dominik Luecke Phone +49-421-218-64265
Dept. of Computer Science Fax +49-421-218-9864265
University of Bremen luecke at informatik.uni-bremen.de
P.O.Box 330440, D-28334 Bremen
PGP-Key ID 0x766B1F6B

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*