Abstract

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.

BibTeX

@incollection{CSRT-AFP10c,
  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{http://afp.sf.net/entries/Abstract-Rewriting.shtml}",
  year        = 2010,
  month       = Aug,
  note        = "Formal proof development"
  ISSN        = "2150-914x", 
}