{"id":1674,"date":"2011-11-09T15:36:58","date_gmt":"2011-11-09T15:36:58","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/li2011-12-formales-normales-y-resolucion-proposicional\/"},"modified":"2013-03-08T05:49:00","modified_gmt":"2013-03-08T05:49:00","slug":"li2011-12-formales-normales-y-resolucion-proposicional","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/li2011-12-formales-normales-y-resolucion-proposicional\/","title":{"rendered":"LI2011-12: Formales normales y resoluci\u00f3n proposicional"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-11\">L\u00f3gica Inform\u00e1tica<\/a> se hemos continuado la b\u00fasqueda de m\u00e9todos autom\u00e1ticos para el problema TAUT (i.e. decidir si una f\u00f3rmula dada es una tautolog\u00eda) y el problema SAT (i.e decidir si una f\u00f3rmula dada es satisfacible). <\/p>\n<p>Comenzamos observando que:<\/p>\n<ul>\n<li> el problema TAUT se resuelve f\u00e1cilmente para las f\u00f3rmulas que son conjunciones de disyunciones de literales (es decir, est\u00e1n en forma normal conjuntiva (FNC)) y\n<li> el problema SAT se resuelve f\u00e1cilmente para las f\u00f3rmulas que son disyunciones de conjunciones de literales (es decir, est\u00e1n en forma normal disyuntiva (FND)).\n<\/ul>\n<p>Por tanto, <\/p>\n<ul>\n<li> para la soluci\u00f3n del problema TAUT s\u00f3lo nos falta un procedimiento mec\u00e1nico que dada una f\u00f3rmula calcule otra que sea equivalente a la dada y que est\u00e9 en FNC y\n<li> para la soluci\u00f3n del problema SAT s\u00f3lo nos falta un procedimiento mec\u00e1nico que dada una f\u00f3rmula calcule otra que sea equivalente a la dada y que est\u00e9 en FND.\n<\/ul>\n<p>Mostramos las reglas de equivalencia para el c\u00e1lculo de los formas normales y los procedimientos de decisi\u00f3n para los porblemas TAUT y SAT.<\/p>\n<p>Adem\u00e1s, vemos c\u00f3mo el m\u00e9todo de los tableros sem\u00e1nticos proporciona otro procedimiento de c\u00e1lculo de las formas normales.<\/p>\n<p>Comenzamos la segunda parte de la clase, observando que, a partir de la forma normal conjuntiva, podemos representar las f\u00f3rmulas, y los conjuntos de f\u00f3rmulas, mediante conjunto de conjuntos de literales. Con esta nueva representaci\u00f3n, basta una \u00fanica regla de demostraci\u00f3n: la regla de resoluci\u00f3n. Esta regla engloba distintas reglas (como modus pones, modus tollens y encadenamiento).<\/p>\n<p>Mediante las cl\u00e1usulas, el problema de inconsistencia de un conjunto de de f\u00f3rmulas se reduce al de la inconsistencia de un conjunto de cl\u00e1usulas.<\/p>\n<p>Mediante resoluci\u00f3n, el problema de la inconsistencia de un conjunto de cl\u00e1usulas se reduce a buscar la cl\u00e1usula vac\u00eda entre las resolventes del conjunto S.<\/p>\n<p>Mostramos un primer algoritmo de b\u00faequeda de la cl\u00e1usula vac\u00eda: el de saturaci\u00f3n y dos mejoras: eliminaci\u00f3n de tautolog\u00edas y de subsumsuci\u00f3n. <\/p>\n<p>Como tarea pendientes se propone la resoluci\u00f3n de los ejercicios de los temas 4 y 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 del<a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-11\/temas\/tema-4.pdf\">tema 4<\/a> y del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-11\/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\/7347967' width='1290' height='1057' sandbox=\"allow-popups allow-scripts allow-same-origin allow-presentation\" allowfullscreen webkitallowfullscreen mozallowfullscreen><\/iframe><\/div><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 primera parte de la clase de hoy del curso L\u00f3gica Inform\u00e1tica se hemos continuado la b\u00fasqueda de m\u00e9todos autom\u00e1ticos para el problema TAUT (i.e. decidir si una f\u00f3rmula dada es una tautolog\u00eda) y el problema SAT (i.e decidir si una f\u00f3rmula dada es satisfacible). Comenzamos observando que: el problema TAUT se resuelve f\u00e1cilmente&#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":[183],"tags":[182],"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\/1674"}],"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=1674"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1674\/revisions"}],"predecessor-version":[{"id":2918,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1674\/revisions\/2918"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1674"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1674"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1674"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}