{"id":3450,"date":"2013-07-27T06:24:00","date_gmt":"2013-07-27T06:24:00","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3450"},"modified":"2013-07-27T06:24:00","modified_gmt":"2013-07-27T06:24:00","slug":"resena-reading-an-algebra-textbook-by-translating-it-to-a-formal-document-in-the-isabelleisar-language","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-reading-an-algebra-textbook-by-translating-it-to-a-formal-document-in-the-isabelleisar-language\/","title":{"rendered":"Rese\u00f1a: Reading an algebra textbook (by translating it to a formal document in the Isabelle\/Isar language)"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo sobre formalizaci\u00f3n en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/Isar<\/a> titulado <a href=\"http:\/\/ceur-ws.org\/Vol-1010\/paper-07.pdf\">Reading an algebra textbook<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/clemens\/\">Clemens Ballarin<\/a> (de la <i>Technische Universit\u00e4t M\u00fcnchen<\/i>) y lo present\u00f3 en el <a href=\"http:\/\/cicm-conference.org\/2013\">CICM 2013<\/a> (<i>Conferences on Intelligent Computer Mathematics<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe report on a formalisation experiment where excerpts from <a href=\"http:\/\/books.google.es\/books\/about\/Basic_Algebra_I.html?id=JHFpv0tKiBAC&#038;redir_esc=y\">an algebra textbook<\/a> are compared to their translation into formal texts of the Isabelle\/Isar prover, and where an attempt is made in the formal text to stick as closely as possible with the structure of the informal counterpart. The purpose of the exercise is to gain understanding on how adequately a modern algebra text can be represented using the module facilities of Isabelle. Our initial results are promising.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobre formalizaci\u00f3n en Isabelle\/Isar titulado Reading an algebra textbook. Su autor es Clemens Ballarin (de la Technische Universit\u00e4t M\u00fcnchen) y lo present\u00f3 en el CICM 2013 (Conferences on Intelligent Computer Mathematics). Su resumen es We report on a formalisation experiment where excerpts from an algebra textbook are compared to their&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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":[89,85,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\/3450"}],"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=3450"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3450\/revisions"}],"predecessor-version":[{"id":3451,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3450\/revisions\/3451"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3450"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3450"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3450"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}