[isabelle-dev] the “algebra" proof method

[Amine Chaieb]

Hi,

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

I could send the Latex Sources from my thesis and add a few lines on the 
method itself (attributes, installing it etc). The latter is perhaps 
subject to change when you change integration in arith?


> 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.
As Tobias mentioned, the method is applicable for more general 
structures. Of course the main application are arithmetic domains nat, 
int, real, complex etc...

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.

The method once installed for a locale, it generates simprocs, 
conversions, etc that could be used. So I would not suggest cutting it 
completely out in favour of an arith-like integration. But as a 
complementary method inside arith it could serve the users well.

> 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 don't think the problem is complex at all. What I suggested is of 
software engineering nature. The student does not need to know about 
Groebner bases at all. The present code has four easily identifiable 
code sections:

  a) Preprocessing the goals into a normal form ---

  b) from the normal form prepare a question to be asked to a Groebner 
bases engine

  c) Groebner Bases engine accepts a question (radical ideal membership) 
and in success returns a certificate for this membership. The 
certificate has a very easy format

  d) in case of success, replay the certificate to create a proof of the 
goal

What i have suggested is to replace (or give more possibilities) for c), 
if that is at all desirable for efficiency reasons. I suggested this, 
because I suspect that you are trying to solve problems from engineering 
or similar fields, where the problems generated are generally much 
larger than typical verification problems.

Similar to what happened with Sledgehammer, SOS, (and Z3?), one could 
use an online service for such problems (again if there is need at all) 
or create one if wanted. Beware however, that the answers to requests 
can be exponentially larger than requests :)

Hope this helps,
Amine.

-- 

                               _
                            _ooOoo_
                           o8888888o
                           88" . "88
                           (| -_- |)
                           O\  =  /O
                        ____/`---'\____
                      .'  \\|     |//  `.
                     /  \\|||  :  |||//  \
                    /  _||||| -:- |||||_  \
                    |   | \\\  -  /'| |   |
                    | \_|  `\`---'//  |_/ |
                    \  .-\__ `-. -'__/-.  /
                  ___`. .'  /--.--\  `. .'___
               ."" '<  `.___\_<|>_/___.' _> \"".
              | | :  `- \`. ;`. _/; .'/ /  .' ; |
              \  \ `-.   \_\_`. _.'_/_/  -' _.' /
    ===========`-.`___`-.__\ \___  /__.-'_.'_.-'================
                            `=--=-'                    hjw