Email Gateway (Aug 18 2022 at 15:47): Email Gateway (Aug 18 2022 at 15:47):From: Tobias Nipkow <nipkow@in.tum.de>
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
interpretations.
http://afp.sourceforge.net/entries/Polynomials.shtml
Thanks to the authors for sharing!
Last updated: Apr 26 2024 at 01:06 UTC