{"id":4405,"date":"2014-09-11T06:00:34","date_gmt":"2014-09-11T04:00:34","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4405"},"modified":"2014-09-07T12:59:08","modified_gmt":"2014-09-07T10:59:08","slug":"resena-real-valued-special-functions-upper-and-lower-bounds","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-real-valued-special-functions-upper-and-lower-bounds\/","title":{"rendered":"Rese\u00f1a: Real-valued special functions: upper and lower bounds"},"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> titulado <a href=\"http:\/\/afp.sourceforge.net\/entries\/Special_Function_Bounds.shtml\">Real-valued special functions: upper and lower bounds<\/a><\/p>\n<p>Su autor es <a href=\"http:\/\/www.cl.cam.ac.uk\/~lp15\">Lawrence C. Paulson<\/a> (de la Universidad de Cambridge).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  <em>This development proves upper and lower bounds for several familiar real-valued functions. For sin, cos, exp and sqrt, it defines and verifies infinite families of upper and lower bounds, mostly based on Taylor series expansions. For arctan, ln and exp, it verifies a finite collection of upper and lower bounds, originally obtained from the functions&#8217; continued fraction expansions using the computer algebra system Maple. A common theme in these proofs is to take the difference between a function and its approximation, which should be zero at one point, and then consider the sign of the derivative. The immediate purpose of this development is to verify axioms used by MetiTarski, an automatic theorem prover for real-valued special functions. Crucial to MetiTarski&#8217;s operation is the provision of upper and lower bounds for each function of interest.<\/em>\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado en en <a href=\"http:\/\/afp.sourceforge.net\">AFP<\/a> (<em>The Archive of Formal Proofs<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas se encuentra <a href=\"http:\/\/afp.sourceforge.net\/release\/afp-Special_Function_Bounds-current.tar.gz\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado Real-valued special functions: upper and lower bounds Su autor es Lawrence C. Paulson (de la Universidad de Cambridge). Su resumen es This development proves upper and lower bounds for several familiar real-valued functions. For sin, cos, exp and sqrt, it defines and verifies infinite&#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":[1],"tags":[166,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\/4405"}],"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=4405"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4405\/revisions"}],"predecessor-version":[{"id":4406,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4405\/revisions\/4406"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4405"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4405"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4405"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}