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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
