{"id":3345,"date":"2013-05-15T17:49:35","date_gmt":"2013-05-15T17:49:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3345"},"modified":"2013-05-19T17:49:59","modified_gmt":"2013-05-19T17:49:59","slug":"lmf2013-resolucion-proposicional-en-haskell","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-resolucion-proposicional-en-haskell\/","title":{"rendered":"LMF2013: Resoluci\u00f3n proposicional en Haskell"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-12\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> (de 3\u00ba de Grado en Matem\u00e1ticas) se ha comentado las soluciones de los ejercicios sobre la implementaci\u00f3n en Haskell de la resoluci\u00f3n proposicional.<\/p>\n<p>Las soluciones de los ejercicios se muestran a continuaci\u00f3n. En los ejercicios se usa los m\u00f3dulos<\/p>\n<ul>\n<li> <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-sintaxis-y-semantica-de-la-logica-proposicional-en-haskell\/\">SintaxisSemantica<\/a>,\n<li> <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-formas-normales-conjuntivas-y-disyuntivas-en-haskell\/\">FormasNormales<\/a> y\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-clausulas-en-haskell\/\">Clausulas<\/a>\n<\/ul>\n<p>desaroolado en clases anteriores.<\/p>\n<p>La implementaci\u00f3n de resoluci\u00f3n comentada es<\/p>\n<pre lang=\"haskell\">\r\nmodule ResolucionProposicional where\r\n\r\nimport SintaxisSemantica\r\nimport FormasNormales\r\nimport Clausulas\r\nimport Data.List\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Resolventes                                                        --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1: Definir la funci\u00f3n\r\n--    resolvente :: Clausula -> Clausula -> Literal -> Clausula\r\n-- tal que (resolvente c1 c2 l) es la resolvente de c1 y c2 respecto del\r\n-- literal l. Por ejemplo,\r\n--    resolvente [no p,q] [no q,r] q  ==>  [no p,r]\r\n--    resolvente [no p,no q] [q,r] (no q)  ==>  [no p,r]\r\n--    resolvente [no p,q] [no p,no q] q  ==>  [no p]\r\n-- ---------------------------------------------------------------------\r\n\r\nresolvente :: Clausula -> Clausula -> Literal -> Clausula\r\nresolvente c1 c2 l =\r\n    union (delete l c1) (delete (complementario l) c2) \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2: Definir la funci\u00f3n\r\n--    resolventes :: Clausula -> Clausula -> [Clausula]\r\n-- tal que (resolventes c1 c2) es el conjunto de las resolventes de c1 y\r\n-- c2. Por ejemplo,\r\n--    resolventes [no p,q] [p,no q]  ==>  [[q,no q],[no p,p]]\r\n--    resolventes [no p,q] [p,q]     ==>  [[q]]\r\n-- ---------------------------------------------------------------------\r\n\r\nresolventes :: Clausula -> Clausula -> [Clausula]\r\nresolventes c1 c2 =\r\n    [resolvente c1 c2 l | l <- c1, (complementario l) `elem` c2]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3: Definir la funci\u00f3n\r\n--    resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]\r\n-- tal que (resolventes c s) es el conjunto de las resolventes de c y\r\n-- s. Por ejemplo, \r\n--    resolventesClausulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]\r\n--    ==> [[q],[q,r],[no p,s]]\r\n-- ---------------------------------------------------------------------\r\n\r\nresolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]\r\nresolventesClausulaConjunto c s =\r\n    unionGeneral [resolventes c c1 | c1 <- s]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Eliminaci\u00f3n de tautolog\u00edas                                         --\r\n-- ---------------------------------------------------------------------\r\n \r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1: Definir la funci\u00f3n\r\n--    esTautologia :: Cl\u00e1usula -> Bool\r\n-- tal que (esTautologia c) se verifica si c es una tautolog\u00eda. Por\r\n-- ejemplo, \r\n--    esTautologia [p, q, no p]  ==>  True\r\n--    esTautologia [p, q, no r]  ==>  False\r\n--    esTautologia []            ==>  False\r\n-- ---------------------------------------------------------------------\r\n\r\nesTautologia :: Clausula -> Bool\r\nesTautologia c = \r\n    [f | f <- c, elem (complementario f) c] \/= []\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2: Definir la funci\u00f3n\r\n--    eliminaTautologias :: [Cl\u00e1usula] -> [Cl\u00e1usula]\r\n-- tal que (eliminaTautologias s) es el conjunto obtenido eliminando las\r\n-- tautolog\u00edas de s. Por ejemplo,\r\n--    eliminaTautologias [[p, q], [p, q, no p]]  ==>  [[p,q]]\r\n-- ---------------------------------------------------------------------\r\n\r\neliminaTautologias :: [Clausula] -> [Clausula]\r\neliminaTautologias s =\r\n    [c | c <- s, not (esTautologia c)]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Decisi\u00f3n de inconsistencia por resoluci\u00f3n                          --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4: Definir la funci\u00f3n\r\n--    esInconsistentePorResolucion :: [Clausula] -> Bool\r\n-- tal que (esInconsistentePorResolucion s) se verifica si s es\r\n-- inconsistente mediante resoluci\u00f3n. Por ejemplo,\r\n--    esInconsistentePorResolucion [[p],[no p,q],[no q]]\r\n--    ==> True\r\n--    esInconsistentePorResolucion [[p],[no p,q]]\r\n--    ==> False\r\n--    esInconsistentePorResolucion [[p,q],[no p,q],[p,no q],[no p,no q]]\r\n--    ==> True\r\n--    esInconsistentePorResolucion [[p,q],[p,r],[no q,no r],[no p]]\r\n--    ==> True\r\n-- ---------------------------------------------------------------------\r\n\r\nesInconsistentePorResolucion :: [Clausula] -> Bool\r\nesInconsistentePorResolucion s =\r\n    esInconsistentePorResolucion' s []\r\n\r\nesInconsistentePorResolucion' :: [Clausula] -> [Clausula] -> Bool\r\nesInconsistentePorResolucion' soporte usables \r\n    | null soporte    = False\r\n    | elem [] soporte = True\r\n    | otherwise       =\r\n        esInconsistentePorResolucion' soporte' usables'\r\n        where actual   = head soporte\r\n              usables' = union [actual] usables\r\n              soporte' = union (tail soporte)\r\n                               [c \r\n                                | c <- resolventesClausulaConjunto\r\n                                       actual \r\n                                       usables'\r\n                                , not (esTautologia c)\r\n                                , notElem c soporte\r\n                                , notElem c usables']\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Validez mediante resoluci\u00f3n                                        --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 5: Definir la funci\u00f3n\r\n--    esValidaPorResoluci\u00f3n :: Prop -> Bool\r\n-- tal que (esValidaPorResoluci\u00f3n f) se verifica si f es v\u00e1lida por\r\n-- resoluci\u00f3n. Por ejemplo, \r\n--    esValidaPorResoluci\u00f3n (p --> p)                 ==>  True\r\n--    esValidaPorResoluci\u00f3n ((p --> q) \\\/ (q --> p))  ==>  True\r\n--    esValidaPorResoluci\u00f3n (p --> q)                 ==>  False\r\n-- ---------------------------------------------------------------------\r\n\r\nesValidaPorResoluci\u00f3n :: Prop -> Bool\r\nesValidaPorResoluci\u00f3n f =\r\n    esInconsistentePorResolucion \r\n    (eliminaTautologias (clausulas (Neg f)))\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Consecuencia mediante resoluci\u00f3n                                   --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 6: Definir la funci\u00f3n\r\n--    esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool\r\n-- tal que (esConsecuenciaPorResolucion s f) se verifica si f es\r\n-- consecuencia de s mediante el m\u00e9todo de resoluci\u00f3n. Por ejemplo,\r\n--    esConsecuenciaPorResolucion [p --> q, q --> r] (p --> r)  \r\n--    ==> True\r\n--    esConsecuenciaPorResolucion [p --> q, q --> r] (p <--> r)\r\n--    ==> False\r\n-- ---------------------------------------------------------------------\r\n\r\nesConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool\r\nesConsecuenciaPorResolucion s f =\r\n    esInconsistentePorResolucion \r\n    (eliminaTautologias (clausulasConjunto ((Neg f):s)))\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy del curso de L\u00f3gica matem\u00e1tica y fundamentos (de 3\u00ba de Grado en Matem\u00e1ticas) se ha comentado las soluciones de los ejercicios sobre la implementaci\u00f3n en Haskell de la resoluci\u00f3n proposicional. Las soluciones de los ejercicios se muestran a continuaci\u00f3n. En los ejercicios se usa los m\u00f3dulos&#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\/3345"}],"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=3345"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3345\/revisions"}],"predecessor-version":[{"id":3346,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3345\/revisions\/3346"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3345"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3345"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3345"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}