{"id":3761,"date":"2013-10-18T16:29:39","date_gmt":"2013-10-18T14:29:39","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3761"},"modified":"2013-10-21T09:31:04","modified_gmt":"2013-10-21T07:31:04","slug":"li2013-formales-normales-conjuntivas-y-disyuntivas","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/li2013-formales-normales-conjuntivas-y-disyuntivas\/","title":{"rendered":"LI2013: Formales normales conjuntivas y disyuntivas"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-13\">L\u00f3gica Inform\u00e1tica<\/a> 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 equivalencia para el c\u00e1lculo de los formas normales y los procedimientos de decisi\u00f3n para los porblemas TAUT y SAT.<\/p>\n<p>Tambi\u00e9n vimos c\u00f3mo el m\u00e9todo de los tableros sem\u00e1nticos proporciona otro procedimiento de c\u00e1lculo de las formas normales.<\/p>\n<p>Las transparencias de esta clase son las del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-13\/temas\/tema-4.pdf\">tema 4<\/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><\/p>\n<p>En la segunda parte de la clase, comentamos las soluciones de los ejercicios de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/ejerciciosLI2013G2\/index.php5\/Relaci\u00f3n_7\">relaci\u00f3n 7<\/a> y se propuso como tarea para la pr\u00f3xima clase los de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/ejerciciosLI2013G2\/index.php5\/Relaci\u00f3n_8\">relaci\u00f3n 8<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy del curso L\u00f3gica Inform\u00e1tica 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 para&#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":[223],"tags":[301,189],"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\/3761"}],"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=3761"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3761\/revisions"}],"predecessor-version":[{"id":3762,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3761\/revisions\/3762"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3761"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3761"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3761"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}