[isabelle-dev] the “algebra" proof method

Lawrence Paulson lp15 at cam.ac.uk
Fri Aug 24 12:33:21 CEST 2012

This sounds like a good plan. And thanks for your further details about how to integrate an external Gröbner basis tool. Do you think this might be of a suitable level of difficulty for an MPhil student?

I also noticed the paper that you presented in Birmingham in 2008. Has that worked been integrated with Isabelle?

On 22 Aug 2012, at 10:24, Amine Chaieb <amine at chaieb.org> wrote:

> I think there should be no harm in adding an arith catcher to handle such problems, while keeping the algebra method itself for cases where the problem is not arithmetic in nature.

More information about the isabelle-dev mailing list