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


Lutz Schroeder asked a very similar similar question on 19 Oct 2007, I
am adding the reference here:


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.


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.