{"id":3313,"date":"2013-05-07T16:23:22","date_gmt":"2013-05-07T16:23:22","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3313"},"modified":"2013-05-08T16:23:41","modified_gmt":"2013-05-08T16:23:41","slug":"lmf2013-estrategias-de-resolucion-proposicional","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-estrategias-de-resolucion-proposicional\/","title":{"rendered":"LMF2013: Estrategias de resoluci\u00f3n proposicional"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-12\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> hemos continuado la b\u00fasqueda de la automatizaci\u00f3n del razonamiento.<\/p>\n<p>Despu\u00e9s de haber visto en la clase anterior el algoritmo de resoluci\u00f3n por saturaci\u00f3n, hemos estudiado distintas estrategias cuyo objetivo es mejorar la b\u00fasqueda de la refutaci\u00f3n por resoluci\u00f3n.<\/p>\n<p>Las estrategias estudiadas son la resoluci\u00f3n positiva, la resoluci\u00f3n negativa, la resoluci\u00f3n unitaria, la resoluci\u00f3n por entradas y la resoluci\u00f3n lineal.<\/p>\n<p>Adem\u00e1s, se ha presentado la estrategia por pesos y propagaci\u00f3n unitaria.<\/p>\n<p>Finalmente, como sistema de demostraci\u00f3n por resoluci\u00f3n se ha presentado el <a href=\"http:\/\/www.cs.unm.edu\/~mccune\/prover9\/\">Prover9<\/a>.<\/p>\n<p>Las transparencias de esta clase son las p\u00e1ginas 25 a 37 del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-12\/temas\/tema-5.pdf\">tema 5<\/a><br \/>\n<!--more--><br \/>\n<div class=\"jetpack-video-wrapper\"><iframe src='https:\/\/www.slideshare.net\/slideshow\/embed_code\/10088565' width='1290' height='1057' sandbox=\"allow-popups allow-scripts allow-same-origin allow-presentation\" allowfullscreen webkitallowfullscreen mozallowfullscreen><\/iframe><\/div><\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos hemos continuado la b\u00fasqueda de la automatizaci\u00f3n del razonamiento. Despu\u00e9s de haber visto en la clase anterior el algoritmo de resoluci\u00f3n por saturaci\u00f3n, hemos estudiado distintas estrategias cuyo objetivo es mejorar la b\u00fasqueda de la refutaci\u00f3n por resoluci\u00f3n. Las estrategias estudiadas son la resoluci\u00f3n&#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":[202],"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\/3313"}],"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=3313"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3313\/revisions"}],"predecessor-version":[{"id":3314,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3313\/revisions\/3314"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3313"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3313"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3313"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}