[isabelle-dev] the “algebra" proof method

[Amine Chaieb]

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.

Summed up the method deals with basically two classes of problems:

1) Universal problems over multivariate polynomials in a 
(semi)-ring/field/idom with each of these the capabilities of the method 
are augmented. For this problem class the method is only complete for 
algebraically closed fields, since the underlying method is based on 
Hilbert's Nullstellensatz, where the equivalence only holds for 
algebraically closed fields.
   --- i.e. The problems can contain equations p=0 or disequations q ~= 
0, anywhere, as long as everythin is universal

2) AE problems (Forall Exists). These have a restricted but very useful 
form:

ALL x_1,...,x_n. e1(x_1,..,x_n)=0 &
                          .....
                          em(x_1,...,x_n)=0
    --> EX y_1,...,y_k.  p_11(x_1,...,x_n)*y_1 + ... + 
p_1k(x_1,...,x_n)*y_k =0
                               & ........
                               & p_t1(x_1,...,x_n)*y_1 + ... + 
p_tk(x_1,...,x_n)*y_k =0

Here e_1,..e_n, p_ij are multivariate polynomials only in the variables 
mentioned as arguments.
This method is not complete as a proof method even if without proofs it 
is complete, See John Harrison's paper in CADE 2007 [3].

I had a version which used reflection based on my formalization of 
reflected multivariate polynomials. The main work is the multivariate 
polynomial library, verifying a checker is realaly trivial. This is also 
in my thesis toger with the case for universal problems over the reals 
(with ordering) using Stengle's Positivstellensatz.

The algebra method uses an internal implementation of Groebner-Bases 
computation, which is as you can guess not at all efficient. There are 
packages out there that would compute the groebner bases thousands of 
times faster but not all of them return a certificate for radical-ideal 
membership, which is what you need for algebra. Perhaps a similar 
project to that for Sum ofSquares would be useful here. Who knows, 
perhaps Isabelle could offer an API for its users to solve such problems 
and integrate it with the method.

The method also has some nice attributes and parameters so you can pass 
in some theorems when you call it, here is an example from 
HOL/ex/Groebner_Examples.thy

subsection {* Colinearity is invariant by rotation *}

type_synonym point = "int \<times> int"

definition collinear ::"point \<Rightarrow> point \<Rightarrow> point 
\<Rightarrow> bool" where
   "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
     ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"

lemma collinear_inv_rotation:
   assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<twosuperior> + 
s\<twosuperior> = 1"
   shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
     (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
   using assms
   by (algebra add: collinear_def split_def fst_conv snd_conv)

Hope this helps,
Amine.

PS: If you are interested in Geometry problems, a reflection of Wu's 
method should not be difficult at all. For LCF-style methods there are 
all the tools about pseudo-division of polynomials in the RCF method.

[1] Amine Chaieb and Makarius Wenzel. Context aware Calculation and 
Deduction - Ring Equalities via Gröbner Bases in Isabelle. In M. Kauers, 
M. Kerber, R. Miner, and W. Windsteiger, editors, /CALCULEMUS 2007/, 
volume 4573 of /Lecture Notes in Computer Science/, pages 27-39. 
Springer, 2007.

[2] Amine Chaieb. /Automated methods for formal proofs in simple 
arithmetics and algebra/. PhD thesis, Technische Universität München, 
Germany, April 2008

[3] John Harrison. Automating elementary number-theoretic proofs using 
Grobner
  bases. In Frank Pfenning, editor, Proceedings of CADE 21, volume 4603 of
Lecture Notes in Computer Science, pages 51–66, Bremen, Germany, 2007.
  Springer-Verlag.


On 08/17/2012 01:30 PM, Lawrence Paulson wrote:
> As far as I am aware, we provide no documentation on the “algebra" proof method.
>
> My impression is that this method will prove anything that it can convert to the form
>
> 	p1 = 0 ==> … ==> pn = 0 ==> p = 0
>
> where p1, …, pn, p are polynomials, possibly in multiple variables, over a suitable semiring, including the integers or reals.
>
> I tried this on the new Impossible_Geometry, where it proved to be very powerful. It's a pity to have such a thing almost secret.
>
> Does anybody have specific knowledge of what it does and doesn't do? And where in the documentation should it be covered?
>
> Larry
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


-- 

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