[isabelle-dev] the “algebra" proof method

Lawrence Paulson lp15 at cam.ac.uk
Tue Aug 21 19:48:47 CEST 2012

Many thanks for your very detailed response! I wonder what to do next in terms of documenting this method, and perhaps, developing it further. Is there a latex source for the information you sent?  It could be added to the documentation somewhere: but where?

Or would it make sense to integrate this functionality with the much better known arith method? It could then be a catchall for whatever else gets implemented in the general realm of arithmetic. And this reminds me that we have a great variety of different arithmetic decision procedures, which I imagine can all be invoked via arith, so maybe it indeed makes sense to add your algebraic procedures to arith.

Then there are your other research suggestions regarding the computation of a Gröbner basis. I'm guessing there that this would take a Ph.D. student due to the complexity of the topic itself as well as the need to get to grips with the existing code.

I would be grateful for any body's thoughts on these topics.


On 18 Aug 2012, at 13:23, Amine Chaieb <amine at chaieb.org> wrote:

> Hi Larry,
> I am glad this method was helpful at last :)
> The algebra proof-method has indeed a very poor Marketing history. Neither the method itself nor the really new aspects of its integration in the Isar Framework were publicized and well documented.
> The original paper for this is work with Makarius in [1]. More details on the capabilities of algebra (not the Isar part) are only in my thesis [2] in Chapter 3.2.

More information about the isabelle-dev mailing list