{"id":4995,"date":"2015-08-28T07:24:50","date_gmt":"2015-08-28T05:24:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4995"},"modified":"2015-08-28T07:25:17","modified_gmt":"2015-08-28T05:25:17","slug":"landau-symbols-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/landau-symbols-en-isabellehol\/","title":{"rendered":"Rese\u00f1a: Landau symbols en Isabelle\/HOL"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> sobre algor\u00edtmica titulado <a href=\"http:\/\/afp.sourceforge.net\/browser_info\/current\/AFP\/Landau_Symbols\/document.pdf\">Landau symbols en Isabelle\/HOL<\/a>.<\/p>\n<p>Sus autor es <a href=\"http:\/\/home.in.tum.de\/~eberlm\">Manuel Eberl<\/a> (del <a href=\"http:\/\/www21.in.tum.de\/\">Theorem Proving Group<\/a> en la <em>Technische Universit\u00e4t M\u00fcnchen<\/em>, Munich, Alemania).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  This entry provides Landau symbols to describe and reason about the asymptotic growth of functions for sufficiently large inputs. A number of simplification procedures are provided for additional convenience: cancelling of dominated terms in sums under a Landau symbol, cancelling of common factors in products, and a decision procedure for Landau expressions containing products of powers of functions like x, ln(x), ln(ln(x)) etc.\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado en <a href=\"http:\/\/afp.sourceforge.net\/entries\/Landau_Symbols.shtml\">The Archive of Formal Proofs<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/afp.sourceforge.net\/browser_info\/current\/AFP\/Landau_Symbols\/index.html\">aqu\u00ed<\/a>.<\/p>\n<p>Este trabajo puede servir como lectura complementaria del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\/\">Razonamiento autom\u00e1tico<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre algor\u00edtmica titulado Landau symbols en Isabelle\/HOL. Sus autor es Manuel Eberl (del Theorem Proving Group en la Technische Universit\u00e4t M\u00fcnchen, Munich, Alemania). Su resumen es This entry provides Landau symbols to describe and reason about the asymptotic growth of functions for sufficiently large inputs&#8230;.<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","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":[144,285],"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\/4995"}],"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=4995"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4995\/revisions"}],"predecessor-version":[{"id":4996,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4995\/revisions\/4996"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4995"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4995"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4995"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}