[isabelle-dev] the “algebra" proof method
Amine Chaieb
amine at chaieb.org
Sat Aug 18 14:23:10 CEST 2012
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
More information about the isabelle-dev
mailing list