*To*: Dominik Luecke <luecke at informatik.uni-bremen.de>*Subject*: Re: [isabelle] Isabelle and Computer Algebra (revisted) / Large Proof Goals*From*: Tjark Weber <webertj at in.tum.de>*Date*: Sun, 22 Feb 2009 01:17:53 +0000*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>

Dominik, On Tue, 2009-02-17 at 10:38 +0100, Dominik Luecke wrote: > 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. 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

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

- Previous by Date: [isabelle] Maps
- Next by Date: Re: [isabelle] Maps
- Previous by Thread: Re: [isabelle] Isabelle and Computer Algebra (revisted) / Large Proof Goals
- Next by Thread: [isabelle] Inductive set and tutorial
- 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