Executable Multivariate Polynomials

Title:	Executable Multivariate Polynomials
Author:	Christian Sternagel and René Thiemann
Submission date:	2010-08-10
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.
Change history:	[2010-09-17]: Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.
BibTeX:	@article{Polynomials-AFP, author = {Christian Sternagel and René Thiemann}, title = {Executable Multivariate Polynomials}, journal = {Archive of Formal Proofs}, month = aug, year = 2010, note = {\url{http://isa-afp.org/entries/Polynomials.shtml}, Formal proof development}, ISSN = {2150-914x}, }
License:	GNU Lesser General Public License (LGPL)
Depends on:	Abstract-Rewriting, Matrix
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.