*To*: Dominik Luecke <luecke at informatik.uni-bremen.de>*Subject*: Re: [isabelle] Isabelle and Computer Algebra (revisted) / Large Proof Goals*From*: Sascha Boehme <boehmes at in.tum.de>*Date*: Tue, 17 Feb 2009 14:37:41 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Till Mossakowski <Till.Mossakowski at dfki.de>*In-reply-to*: <499A857D.2000402@informatik.uni-bremen.de>*References*: <499A857D.2000402@informatik.uni-bremen.de>*User-agent*: Mutt/1.5.16 (2007-06-09)

Hi Dominik, Concerning huge assumptions in proof goals, we might be working on a solution. Could you please be more precise about what kind of goals you are facing? Alternatively, you could also send me a (collection of) representative example(s). Regards, Sascha Dominik Luecke wrote: > 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

**References**:**[isabelle] Isabelle and Computer Algebra (revisted) / Large Proof Goals***From:*Dominik Luecke

- Previous by Date: [isabelle] Inductive set and tutorial
- Next by Date: Re: [isabelle] Inductive set and tutorial
- Previous by Thread: [isabelle] Isabelle and Computer Algebra (revisted) / Large Proof Goals
- Next by Thread: Re: [isabelle] Isabelle and Computer Algebra (revisted) / Large Proof Goals
- Cl-isabelle-users February 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list