Executable Multivariate Polynomials

Christian Sternagel and René Thiemann

The Archive of Formal Proofs, 2010.


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 tech-niques. The provided theories have been essential to formalize polynomial interpretations.


   AFP entry


author = "Christian Sternagel and Ren{\'e} Thiemann",
title = "{E}xecutable {M}ultivariate {P}olynomials",
booktitle = "The Archive of Formal Proofs",
editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
publisher = "\url{}",
year = 2010,
month = Aug,
note = "Formal proof development"
ISSN = "2150-914x",
Nach oben scrollen