[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.