Executable Multivariate Polynomials
Christian Sternagel y René Thiemann han publicado en The Archive of Formal Proofs el artículo Executable Multivariate Polynomials.
El artículo es parte del proyecto IsaFoR/CeTA (Isabelle Formalization of Rewriting / Certified Termination Analysis) cuyo objetivo es la formalización en Isabelle de técnicas de terminación. Los ficheros del proyecto se encuentran aquí.
Una de las técnicas usadas para demostrar la terminación de sistemas de reescritura se basa en las interpretaciones polinómicas.
En el artículo Executable Multivariate Polynomials se presenta una formalización en Isabelle de los polinomios con varias variables con coeficientes en un semianillo ordenado. Se definen las operaciones de polinomios (suma, multiplicación y sustitución) y la ordenación de polinomios. La formalización también incluye el criterio de Neurauter, Zankl y Middeldorp monotocidad de interpretaciones polinómicas sobre los naturales.