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



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





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