{"id":2321,"date":"2012-11-13T16:48:49","date_gmt":"2012-11-13T16:48:49","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2321"},"modified":"2013-03-08T05:47:39","modified_gmt":"2013-03-08T05:47:39","slug":"li2012-estrategias-de-resolucion-proposicional","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/li2012-estrategias-de-resolucion-proposicional\/","title":{"rendered":"LI2012: Estrategias de resoluci\u00f3n proposicional"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-12\">L\u00f3gica Inform\u00e1tica<\/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>Como tarea se propone la resoluci\u00f3n de los ejercicios del tema 5 del <a href=\"http:\/\/www.cs.y us.es\/~jalonso\/cursos\/li-10\/temas\/ejercicios-LI-2011-12.pdf\">libro de ejercicios<\/a>.\n<\/ul>\n<p>Las transparencias de esta clase son las p\u00e1ginas 25 a 37 del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-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 Inform\u00e1tica 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 positiva, la&#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":[],"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\/2321"}],"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=2321"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2321\/revisions"}],"predecessor-version":[{"id":2751,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2321\/revisions\/2751"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2321"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2321"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2321"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}