Disappointing, but not too surprising. Ah well, back to the drawing board :) Thanks!

I see, thanks! Could you elaborate on where my line of reasoning (from integral domains to integers to nonnegative integers, assuming the slides are correct) breaks down, though?

Well, the main semiring I care about is the naturals with the usual addition and multiplication (actual multiplication, not the weakened form in that omega Presburger solver tactic, that just expands constant multiplicands), so nothing exotic. Mostly was just curious how general such a solver could be though. Superficially, I'd like something that can tell me things like: forall x. x < x + 1 is true forall x y. x <= y is unknown So really, something that leads to a partial order of polynomials over an arbitrary instance of an (ideally fairly weak) algebraic structure.