{"id":405,"date":"2010-08-11T16:16:15","date_gmt":"2010-08-11T16:16:15","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/executable-multivariate-polynomials\/"},"modified":"2013-03-08T05:53:42","modified_gmt":"2013-03-08T05:53:42","slug":"executable-multivariate-polynomials","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/executable-multivariate-polynomials\/","title":{"rendered":"Executable Multivariate Polynomials"},"content":{"rendered":"<p><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/griff\/\">Christian Sternagel<\/a> y <a href=\"http:\/\/cl-informatik.uibk.ac.at\/~thiemann\/\">Ren\u00e9 Thiemann<\/a> han publicado en The Archive of Formal Proofs el art\u00edculo <a href=\"http:\/\/afp.sourceforge.net\/entries\/Polynomials.shtml\">Executable Multivariate Polynomials<\/a>.<\/p>\n<p>El art\u00edculo es parte del proyecto <a href=\"http:\/\/cl-informatik.uibk.ac.at\/software\/ceta\/\">IsaFoR\/CeTA (Isabelle Formalization of Rewriting \/ Certified Termination Analysis)<\/a> cuyo objetivo es la formalizaci\u00f3n en Isabelle de t\u00e9cnicas de terminaci\u00f3n. Los ficheros del proyecto se encuentran <a href=\"http:\/\/cl2-informatik.uibk.ac.at\/rewriting\/mercurial.cgi\/CeTA\/IsaFoR\">aqu\u00ed<\/a>.<\/p>\n<p>Una de las t\u00e9cnicas usadas para demostrar la terminaci\u00f3n de sistemas de reescritura se basa en las <a href=\"http:\/\/perso.ens-lyon.fr\/pierre.lescanne\/PUBLICATIONS\/termpoly.pdfperso.ens-lyon.fr\/pierre.lescanne\/PUBLICATIONS\/termpoly.pdf\">interpretaciones polin\u00f3micas<\/a>.<\/p>\n<p>En el art\u00edculo <a href=\"http:\/\/afp.sourceforge.net\/entries\/Polynomials.shtml\">Executable Multivariate Polynomials<\/a> se presenta una formalizaci\u00f3n en Isabelle de los polinomios con varias variables con coeficientes en un semianillo ordenado. Se definen las operaciones de polinomios (suma, multiplicaci\u00f3n y sustituci\u00f3n) y la ordenaci\u00f3n de polinomios. La formalizaci\u00f3n tambi\u00e9n incluye el <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/hzankl\/new\/publications\/NE10_01.pdf\">criterio de Neurauter, Zankl y Middeldorp<\/a> monotocidad de interpretaciones polin\u00f3micas sobre los naturales.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Christian Sternagel y Ren\u00e9 Thiemann han publicado en The Archive of Formal Proofs el art\u00edculo Executable Multivariate Polynomials. El art\u00edculo es parte del proyecto IsaFoR\/CeTA (Isabelle Formalization of Rewriting \/ Certified Termination Analysis) cuyo objetivo es la formalizaci\u00f3n en Isabelle de t\u00e9cnicas de terminaci\u00f3n. Los ficheros del proyecto se encuentran aqu\u00ed. Una de las t\u00e9cnicas&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[20,89,85],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/405"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=405"}],"version-history":[{"count":6,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/405\/revisions"}],"predecessor-version":[{"id":3041,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/405\/revisions\/3041"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=405"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=405"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=405"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}