[isabelle] New AFP entry: Executable Multivariate Polynomials

Executable Multivariate Polynomials
Christian Sternagel and René Thiemann

We define multivariate polynomials over arbitrary (ordered) semirings in
combination with (executable) operations like addition, multiplication,
and substitution. We also define (weak) monotonicity of polynomials and
comparison of polynomials where we provide standard estimations like
absolute positiveness or the more recent approach of Neurauter, Zankl,
and Middeldorp. Moreover, it is proven that strongly normalizing
(monotone) orders can be lifted to strongly normalizing (monotone)
orders over polynomials. Our formalization was performed as part of the
IsaFoR/CeTA-system which contains several termination techniques. The
provided theories have been essential to formalize polynomial


Thanks to the authors for sharing!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.