[isabelle-dev] the “algebra" proof method
lp15 at cam.ac.uk
Fri Aug 17 13:30:32 CEST 2012
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?
More information about the isabelle-dev