{"id":2003,"date":"2012-03-27T19:38:09","date_gmt":"2012-03-27T19:38:09","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2003"},"modified":"2013-03-08T05:48:16","modified_gmt":"2013-03-08T05:48:16","slug":"lmf2012-tableros-semanticos-en-haskell","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2012-tableros-semanticos-en-haskell\/","title":{"rendered":"LMF2012: Tableros sem\u00e1nticos en Haskell"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-11\">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 los tableros sem\u00e1nticos.<\/p>\n<p>Las soluciones de los ejercicios se muestran a continuaci\u00f3n. En los ejercicios se usa el m\u00f3dulo SintaxisSemantica desarrollado en la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2012-sintaxis-y-semantica-de-la-logica-proposicional-en-haskell\">clase del d\u00eda 13 de marzo<\/a>.<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\">\r\nmodule TablerosSemanticos where\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Librer\u00edas auxiliares                                               --\r\n-- ---------------------------------------------------------------------\r\n\r\nimport SintaxisSemantica\r\nimport Data.List \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Literales                                                          --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 0: Definir la funci\u00f3n\r\n--    literal :: Prop -> Bool\r\n-- tal que (literal f) se verifica si la f\u00f3rmula F es un literal. Por\r\n-- ejemplo, \r\n--    literal p               ==  True\r\n--    literal (no p)          ==  True\r\n--    literal (no (p --> q))  ==  False\r\n-- ---------------------------------------------------------------------\r\n\r\nliteral :: Prop -> Bool\r\nliteral (Atom f)       = True\r\nliteral (Neg (Atom f)) = True\r\nliteral _              = False\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Notaci\u00f3n uniforme                                                  --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1: Definir la funci\u00f3n\r\n--    dobleNegacion :: Prop -> Bool\r\n-- tal que (dobleNegacion f) se verifica si f es una doble negaci\u00f3n. Por\r\n-- ejemplo, \r\n--    dobleNegacion (no (no p))     ==>  True\r\n--    dobleNegacion (no (p --> q))  ==>  False\r\n-- ---------------------------------------------------------------------\r\n\r\ndobleNegacion :: Prop -> Bool\r\ndobleNegacion (Neg (Neg _)) = True\r\ndobleNegacion _             = False\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2: Definir la funci\u00f3n\r\n--    alfa :: Prop -> Bool\r\n-- tal que (alfa f) se verifica si f es una f\u00f3rmula alfa.\r\n-- ---------------------------------------------------------------------\r\n\r\nalfa :: Prop -> Bool\r\nalfa (Conj _ _)       = True\r\nalfa (Neg (Impl _ _)) = True\r\nalfa (Neg (Disj _ _)) = True\r\nalfa _                = False\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3: Definir la funci\u00f3n\r\n--    beta :: Prop -> Bool\r\n-- tal que (beta d) se verifica si f es una f\u00f3rmula beta.\r\n-- ---------------------------------------------------------------------\r\n\r\nbeta :: Prop -> Bool\r\nbeta (Disj _ _)       = True\r\nbeta (Impl _ _)       = True\r\nbeta (Neg (Conj _ _)) = True\r\nbeta (Equi _ _)       = True\r\nbeta (Neg (Equi _ _)) = True\r\nbeta _                = False\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4: Definir la funci\u00f3n\r\n--    componentes :: Prop -> [Prop]\r\n-- tal que (componentes ) es la lista de las componentes de la f\u00f3rmula\r\n-- f. Por ejemplo, \r\n--    componentes (p \/\\ q --> r)       ==>  [no (p \/\\ q),r]\r\n--    componentes (no (p \/\\ q --> r))  ==>  [(p \/\\ q),no r]\r\n-- ---------------------------------------------------------------------\r\n\r\ncomponentes :: Prop -> [Prop]\r\ncomponentes (Neg (Neg f))    = [f]\r\ncomponentes (Conj f g)       = [f, g]\r\ncomponentes (Neg (Impl f g)) = [f, Neg g]\r\ncomponentes (Neg (Disj f g)) = [Neg f, Neg g]\r\ncomponentes (Disj f g)       = [f, g]\r\ncomponentes (Impl f g)       = [Neg f, g]\r\ncomponentes (Neg (Conj f g)) = [Neg f, Neg g]\r\ncomponentes (Equi f g)       = [Conj f g, Conj (Neg f) (Neg g)]\r\ncomponentes (Neg (Equi f g)) = [Conj f (Neg g), Conj (Neg f) g]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Modelos mediante tableros                                          --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 5: Definir la funci\u00f3n\r\n--    conjuntoDeLiterales :: [Prop] -> Bool\r\n-- tal que (conjuntoDeLiterales fs) se verifica si fs es un conjunto de\r\n-- literales. Por ejemplo, \r\n--    conjuntoDeLiterales [p --> q, no r, r \/\\ s, p]  ==>  False\r\n--    conjuntoDeLiterales [p, no q, r]                ==>  True\r\n-- ---------------------------------------------------------------------\r\n\r\nconjuntoDeLiterales :: [Prop] -> Bool\r\nconjuntoDeLiterales fs =\r\n    and [literal f | f <- fs]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 6: Definir la funci\u00f3n\r\n--    tieneContradiccion :: [Prop] -> Bool\r\n-- tal que (tieneContradiccion fs) se verifica si fs contiene una\r\n-- f\u00f3rmula y su negaci\u00f3n. Por ejemplo,\r\n--    tieneContradiccion [r, p \/\\ q, s, no(p \/\\ q)]  ==>  True\r\n-- ---------------------------------------------------------------------\r\n\r\ntieneContradiccion :: [Prop] -> Bool\r\n-- tieneContradiccion fs \r\n--     | trace (\"  \" ++ show fs) False = undefined\r\ntieneContradiccion fs =\r\n    [f | f <- fs, elem (Neg f) fs] \/= []\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 7: Definir la funci\u00f3n\r\n--    expansionDN :: [Prop] -> Prop -> [[Prop]]\r\n-- tal que (expansionDN fs f) es la expansi\u00f3n de fs mediante la doble\r\n-- negaci\u00f3n f. Por ejemplo,\r\n--    expansionDN [p, no(no q), r] (no(no q))  ==>  [[q,p,r]]\r\n-- ---------------------------------------------------------------------\r\n\r\nexpansionDN :: [Prop] -> Prop -> [[Prop]]\r\nexpansionDN fs f =\r\n    [(componentes f) `union` (delete f fs)]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 8: Definir la funci\u00f3n\r\n--    expansionAlfa :: [Prop] -> Prop -> [[Prop]]\r\n-- tal que (expansionAlfa fs f) es la expansi\u00f3n de fs mediante la\r\n-- f\u00f3rmula alfa f. Por ejemplo,\r\n--    expansionAlfa [q, (p1 \/\\ p2) , r] (p1 \/\\ p2)  ==>  [[p1,p2,q,r]]\r\n-- ---------------------------------------------------------------------\r\n\r\nexpansionAlfa :: [Prop] -> Prop -> [[Prop]]\r\nexpansionAlfa fs f =\r\n    [(componentes f) `union` (delete f fs)]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 9: Definir la funci\u00f3n\r\n--    expansionBeta :: [Prop] -> Prop -> [[Prop]]\r\n-- tal que (expansionBeta fs f) es la expansi\u00f3n de fs mediante la\r\n-- f\u00f3rmula beta f. Por ejemplo,\r\n--    expansionBeta [q, (p1 \\\/ p2) , r] (p1 \\\/ p2)  ==>  [[p1,q,r],[p2,q,r]]\r\n-- ---------------------------------------------------------------------\r\n\r\nexpansionBeta :: [Prop] -> Prop -> [[Prop]]\r\nexpansionBeta fs f =\r\n    [[g] `union` (delete f fs) | g <- componentes f]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10: Definir la funci\u00f3n\r\n--    sucesores :: [Prop] -> [[Prop]]\r\n-- tal que (sucesores fs) es la lista de sucesores de fs. Por ejemplo,\r\n--    sucesores [q \\\/ s, no(no r), p1 \/\\ p2] => [[r,(q \\\/ s),(p1 \/\\ p2)]]\r\n--    sucesores [r,(q \\\/ s),(p1 \/\\ p2)]      => [[p1,p2,r,(q \\\/ s)]]\r\n--    sucesores [p1,p2,r,(q \\\/ s)]           => [[q,p1,p2,r],[s,p1,p2,r]]\r\n-- ---------------------------------------------------------------------\r\n\r\nsucesores :: [Prop] -> [[Prop]]\r\nsucesores fs \r\n    | doblesNegaci\u00f3n \/= []  = expansionDN   fs (head doblesNegaci\u00f3n)\r\n    | alfas \/= []           = expansionAlfa fs (head alfas)\r\n    | betas \/= []           = expansionBeta fs (head betas)\r\n    where doblesNegaci\u00f3n = [f | f <- fs, dobleNegacion f]\r\n          alfas          = [f | f <- fs, alfa f]\r\n          betas          = [f | f <- fs, beta f]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 11: Definir la funci\u00f3n\r\n--    modelosTab :: [Prop] -> [[Prop]]\r\n-- tal que (modelosTab fs) es el conjunto de los modelos de fs\r\n-- calculados mediante el m\u00e9todo de tableros sem\u00e1nticos. Por ejemplo,\r\n--    modelosTab [p --> q, no(q --> p)]  \r\n--    ==> [[no p,q],[q,no p]]\r\n--    modelosTab [p --> q, no q --> no p]  \r\n--    ==> [[q,no p],[no p],[q],[no p,q]]\r\n-- ---------------------------------------------------------------------\r\n\r\nmodelosTab :: [Prop] -> [[Prop]]\r\nmodelosTab fs \r\n    | tieneContradiccion fs  = []\r\n    | conjuntoDeLiterales fs = [fs]\r\n    | otherwise              = unionGeneral [modelosTab gs \r\n                                             | gs <- sucesores fs]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 12: Definir la funci\u00f3n\r\n--    subconjunto :: Eq a => [a] -> [a] -> Bool\r\n-- tal que (subconjunto x y) se verifica si x es subconjunto de y. Por\r\n-- ejemplo, \r\n--    subconjunto [1,3] [3,2,1]    ==>  True\r\n--    subconjunto [1,3,5] [3,2,1]  ==> False\r\n-- ---------------------------------------------------------------------\r\n\r\nsubconjunto :: Eq a => [a] -> [a] -> Bool\r\nsubconjunto xs ys =\r\n    and [elem x ys | x <- xs]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 13: Definir la funci\u00f3n\r\n--    modelosGenerales :: [Prop] -> [[Prop]]\r\n-- tal que (modelosGenerales fs) es el conjunto de los modelos generales\r\n-- de fs calculados mediante el m\u00e9todo de tableros sem\u00e1nticos. Por\r\n-- ejemplo, \r\n--    modelosGenerales [p --> q, no q --> no p]  ==>  [[no p],[q]]\r\n-- ---------------------------------------------------------------------\r\n\r\nmodelosGenerales :: [Prop] -> [[Prop]]\r\nmodelosGenerales fs =\r\n    [gs | gs <- modelos\r\n        , [hs | hs <- delete gs modelos, subconjunto hs gs] == []]\r\n    where modelos = modelosTab fs\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Teoremas por tableros                                              --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 14: Definir la funci\u00f3n\r\n--    esTeoremaPorTableros :: Prop -> Bool\r\n-- tal que (esTeoremaPorTableros f) se verifica si la f\u00f3rmula f es\r\n-- teorema (mediante tableros sem\u00e1nticos). Por ejemplo,  \r\n--    esTeoremaPorTableros (p --> p)  ==>  True\r\n--    esTeoremaPorTableros (p --> q)  ==>  False\r\n-- ---------------------------------------------------------------------\r\n\r\nesTeoremaPorTableros :: Prop -> Bool\r\nesTeoremaPorTableros f =\r\n    modelosTab [Neg f] == []\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Consecuencia por tableros                                          --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 15: Definir la funci\u00f3n\r\n--    esDeduciblePorTableros :: [Prop] -> Prop -> Bool\r\n-- tal que (esDeduciblePorTableros fs f) se verifica si la f\u00f3rmula f es\r\n-- consecuencia (mediante tableros) del conjunto de f\u00f3rmulas fs. Por\r\n-- ejemplo,\r\n--    esDeduciblePorTableros [p --> q, q --> r] (p --> r)   ==>  True\r\n--    esDeduciblePorTableros [p --> q, q --> r] (p <--> r)  ==>  False\r\n-- ---------------------------------------------------------------------\r\n\r\nesDeduciblePorTableros :: [Prop] -> Prop -> Bool\r\nesDeduciblePorTableros fs f =\r\n    modelosTab ((Neg f):fs) == []\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En 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 los tableros sem\u00e1nticos. Las soluciones de los ejercicios se muestran a continuaci\u00f3n. En los ejercicios se usa el m\u00f3dulo SintaxisSemantica desarrollado en 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":[270,192,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\/2003"}],"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=2003"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2003\/revisions"}],"predecessor-version":[{"id":2832,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2003\/revisions\/2832"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2003"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2003"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2003"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}