[isabelle-dev] the “algebra" proof method

Tobias Nipkow nipkow at in.tum.de
Tue Aug 21 21:11:58 CEST 2012


Am 21/08/2012 19:48, schrieb Lawrence Paulson:
> 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.

When I came up with the name "by algebra" I had imagined it to be applicable to
many algebraic structures and to subsume many further proof methods. But given
that it has remained the only such method and that it is used primarily for
arithmetic theories, we might as well call it from "by arith", too.

Tobias



More information about the isabelle-dev mailing list