{"id":4140,"date":"2014-02-18T08:16:13","date_gmt":"2014-02-18T07:16:13","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4140"},"modified":"2014-02-18T08:16:13","modified_gmt":"2014-02-18T07:16:13","slug":"a-survey-of-axiom-selection-as-a-machine-learning-problem","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/a-survey-of-axiom-selection-as-a-machine-learning-problem\/","title":{"rendered":"A survey of axiom selection as a machine learning problem"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo automatizaci\u00f3n del razonamiento en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/www21.in.tum.de\/~blanchet\/axiom_sel.pdf\">A survey of axiom selection as a machine learning problem<\/a>.<\/p>\n<p>Sus autores son <\/p>\n<ul>\n<li><a href=\"http:\/\/www.cs.ru.nl\/~kuehlwein\">Daniel K\u00fchlwein<\/a> (de la Univ. de Nimega, Pa\u00edses Bajos). y\n<li><a href=\"http:\/\/www21.in.tum.de\/~blanchet\">Jasmin Christian Blanchette<\/a> (de la Univ. T\u00e9cnica de Munich, Alemania).\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\nAutomatic theorem provers struggle to discharge proof obligations of interactive theorem provers. This is partly due to the large number of background facts that are passed to the automatic provers as axioms. Axiom selection algorithms predict the relevance of facts, thereby helping to reduce the search space of automatic provers. This paper presents an introduction to axiom selection as a machine learning problem and describes the challenges that distinguish it from other applications of machine learning.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo automatizaci\u00f3n del razonamiento en Isabelle\/HOL titulado A survey of axiom selection as a machine learning problem. Sus autores son Daniel K\u00fchlwein (de la Univ. de Nimega, Pa\u00edses Bajos). y Jasmin Christian Blanchette (de la Univ. T\u00e9cnica de Munich, Alemania). Su resumen es Automatic theorem provers struggle to discharge proof obligations&#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\/4140"}],"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=4140"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4140\/revisions"}],"predecessor-version":[{"id":4141,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4140\/revisions\/4141"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4140"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4140"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4140"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}