[isabelle-dev] the “algebra" proof method

[Lawrence Paulson]

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