{"id":2259,"date":"2012-10-28T06:25:15","date_gmt":"2012-10-28T06:25:15","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2259"},"modified":"2013-03-08T05:44:26","modified_gmt":"2013-03-08T05:44:26","slug":"the-boyer-moore-waterfall-model-revisited","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/the-boyer-moore-waterfall-model-revisited\/","title":{"rendered":"Rese\u00f1a: The Boyer-Moore waterfall model revisited"},"content":{"rendered":"<p>Uno de los problemas fundamentales dentro del campo del razonamiento autom\u00e1tico es la automatizaci\u00f3n de la inducci\u00f3n. El m\u00e9todo fundamental para automatizar la inducci\u00f3n es el de la cascada presentado por <a href=\"http:\/\/www.cs.utexas.edu\/~boyer\">Robert S. Boyer<\/a> y <a href=\"http:\/\/www.cs.utexas.edu\/~moore\">J S. Moore<\/a> en su libro <a href=\"http:\/\/www.cs.utexas.edu\/~boyer\/acl.pdf\">A Computational Logic<\/a> e integrado en sus sistemas <a href=\"http:\/\/www.cs.utexas.edu\/~boyer\/ftp\/nqthm\/index.html\">Nqthm<\/a> y <a href=\"http:\/\/www.cs.utexas.edu\/~moore\/acl2\">ACL2<\/a>.<\/p>\n<p>En el trabajo <a href=\"http:\/\/www.inf.ed.ac.uk\/teaching\/courses\/ar\/slides\/BoyerMoore.pdf\">The Boyer-Moore waterfall model revisited<\/a> se presenta una implementaci\u00f3n del modelo de Boyer-Moore en el sistema <a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/\">HOL Light<\/a>. <\/p>\n<p>Sus autores son <a href=\"http:\/\/homepages.inf.ed.ac.uk\/s0681691\">Petros Papapanagiotou<\/a> y <a href=\"http:\/\/homepages.inf.ed.ac.uk\/jdf\">Jacques Fleuriot<\/a> (de la Universidad de Edimburgo).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nIn this paper, we investigate the potential of the Boyer-Moore waterfall model for the automation of inductive proofs within a modern proof assistant. We analyze the basic concepts and methodology underlying this 30-year-old model and implement a new, fully integrated tool in the theorem prover HOL Light that can be invoked as a tactic. We also describe several extensions and enhancements to the model. These include the integration of existing HOL Light proof procedures and the addition of state-of-the-art generalization techniques into the waterfall. Various features, such as proof feedback and heuristics dealing with non-termination, that are needed to make this automated tool useful within our interactive setting are also discussed. Finally, we present a thorough evaluation of the approach using a set of 150 theorems, and discuss the effectiveness of our additions and relevance of the model in light of our results.<\/p><\/blockquote>\n<p>El trabajo es una extensi\u00f3n de la Tesis de M\u00e1ster de <a href=\"http:\/\/homepages.inf.ed.ac.uk\/s0681691\">Petros Papapanagiotou<\/a> titulada <a href=\"http:\/\/www.inf.ed.ac.uk\/publications\/thesis\/online\/IM070466.pdf\">On the automation of inductive proofs in HOL<br \/>\nLight<\/a> y sirve como lectura complementaria en el curso <a href=\"http:\/\/www.inf.ed.ac.uk\/teaching\/courses\/ar\/slides\">Automated Reasoning (2012-13)<\/a> de la Universidad de Edimburgo. Las transparencias del correspondiente tema del curso son <a href=\"http:\/\/www.inf.ed.ac.uk\/teaching\/courses\/ar\/slides\/induction_lecture.pdf\">Inductive theorem proving<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Uno de los problemas fundamentales dentro del campo del razonamiento autom\u00e1tico es la automatizaci\u00f3n de la inducci\u00f3n. El m\u00e9todo fundamental para automatizar la inducci\u00f3n es el de la cascada presentado por Robert S. Boyer y J S. Moore en su libro A Computational Logic e integrado en sus sistemas Nqthm y ACL2. En el trabajo&#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":[100],"tags":[22,163,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\/2259"}],"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=2259"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2259\/revisions"}],"predecessor-version":[{"id":2642,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2259\/revisions\/2642"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2259"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2259"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2259"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}