{"id":370,"date":"2010-08-08T08:58:26","date_gmt":"2010-08-08T08:58:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formal-power-series\/"},"modified":"2013-03-08T05:53:43","modified_gmt":"2013-03-08T05:53:43","slug":"formal-power-series","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formal-power-series\/","title":{"rendered":"Formal Power Series"},"content":{"rendered":"<p>Acaba de publicarse un nuevo art\u00edculo de razonamiento formalizado. El art\u00edculo es <a href=\"http:\/\/www.springerlink.com\/content\/338870961w221t81\/\">Formal Power Series<\/a> publicado por Amine Chaieb en el Journal of Automated Reasoning.<\/p>\n<p>El resumen que hace el autor del art\u00edculo es el siguiente:\u00a0<em>We present a formalization of the topological ring of formal power series in Isabelle\/HOL. We also formalize formal derivatives, division, radicals, composition and reverses. As an application, we show how formal elementary and hyper-geometric series yield elegant proofs for some combinatorial identities. We easily derive a basic theory of polynomials. Then, using a generic formalization of the fraction field of an integral domain, we obtain formal Laurent series and rational functions for free.<\/em><\/p>\n<p>La formalizaci\u00f3n completa se encuentra en <a href=\"http:\/\/isabelle.in.tum.de\/library\/HOL\/Library\/Formal_Power_Series.html\">Theory Formal Power Series<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Acaba de publicarse un nuevo art\u00edculo de razonamiento formalizado. El art\u00edculo es Formal Power Series publicado por Amine Chaieb en el Journal of Automated Reasoning. El resumen que hace el autor del art\u00edculo es el siguiente:\u00a0We present a formalization of the topological ring of formal power series in Isabelle\/HOL. We also formalize formal derivatives, division,&#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":[1],"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\/370"}],"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=370"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/370\/revisions"}],"predecessor-version":[{"id":3045,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/370\/revisions\/3045"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=370"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=370"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=370"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}