I've been looking at proof techniques in formal systems like Coq and Agda recently, and encountered the `newring`

tactic described here for proving equalities over arbitrary (semi)rings. It does this by reducing the generated polynomials to a Horner normal form and comparing equality over that.

That got me wondering whether a similar approach is possible for inequalities over general "ordered semirings" (where the order fits with the semiring operations). Someone pointed me to the `omega`

tactic in Coq, for proving arbitrary statements (including inequalities) about Presburger arithmetic (with some restricted simulated multiplication). Anyway, it's clearly possible for Presburger arithmetic because all statements are decidable, but I don't really care about all statements, and was wondering whether it was possible for a particular algebraic structure without relying on properties of particular structures like the integers or reals.

Does anyone know whether it is possible to ? I'd be happy to even get some pointers to look more deeply into the problem, as I'm not even sure what to search for at this point.

Thanks!

Edit: there's more on the question in these slides. So I can do it on integral domains and fields through a connection with the reals. I'd really like to do it for arbitrary semirings, though.