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


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.


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