[isabelle-dev] the “algebra" proof method

[Lawrence Paulson]

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?
Larry

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.