{"id":4273,"date":"2014-04-11T14:20:31","date_gmt":"2014-04-11T12:20:31","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4273"},"modified":"2014-04-25T14:25:12","modified_gmt":"2014-04-25T12:25:12","slug":"lmf2014-tableros-semanticos-en-haskell","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2014-tableros-semanticos-en-haskell\/","title":{"rendered":"LMF2014: 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-13\">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>En los ejercicios se usa el m\u00f3dulo SintaxisSemantica desarrollado anteriormente.<\/p>\n<p>Las soluciones de los ejercicios se muestran a continuaci\u00f3n.<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\" title=\"Tableros sem\u00e1nticos\">\nmodule TablerosSemanticos where\n\n-- ---------------------------------------------------------------------\n-- Librer\u00edas auxiliares                                               --\n-- ---------------------------------------------------------------------\n\nimport SintaxisSemantica\nimport Data.List \n\n-- ---------------------------------------------------------------------\n-- Literales                                                          --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 0: Definir la funci\u00f3n\n--    literal :: Prop -> Bool\n-- tal que (literal f) se verifica si la f\u00f3rmula F es un literal. Por\n-- ejemplo, \n--    literal p               ==  True\n--    literal (no p)          ==  True\n--    literal (no (p --> q))  ==  False\n-- ---------------------------------------------------------------------\n\nliteral :: Prop -> Bool\nliteral (Atom f)       = True\nliteral (Neg (Atom f)) = True\nliteral _              = False\n\n-- ---------------------------------------------------------------------\n-- Notaci\u00f3n uniforme                                                  --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 1: Definir la funci\u00f3n\n--    dobleNegacion :: Prop -> Bool\n-- tal que (dobleNegacion f) se verifica si f es una doble negaci\u00f3n. Por\n-- ejemplo, \n--    dobleNegacion (no (no p))     ==>  True\n--    dobleNegacion (no (p --> q))  ==>  False\n-- ---------------------------------------------------------------------\n\ndobleNegacion :: Prop -> Bool\ndobleNegacion (Neg (Neg _)) = True\ndobleNegacion _             = False\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 2: Definir la funci\u00f3n\n--    alfa :: Prop -> Bool\n-- tal que (alfa f) se verifica si f es una f\u00f3rmula alfa.\n-- ---------------------------------------------------------------------\n\nalfa :: Prop -> Bool\nalfa (Conj _ _)       = True\nalfa (Neg (Impl _ _)) = True\nalfa (Neg (Disj _ _)) = True\nalfa _                = False\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 3: Definir la funci\u00f3n\n--    beta :: Prop -> Bool\n-- tal que (beta d) se verifica si f es una f\u00f3rmula beta.\n-- ---------------------------------------------------------------------\n\nbeta :: Prop -> Bool\nbeta (Disj _ _)       = True\nbeta (Impl _ _)       = True\nbeta (Neg (Conj _ _)) = True\nbeta (Equi _ _)       = True\nbeta (Neg (Equi _ _)) = True\nbeta _                = False\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 4: Definir la funci\u00f3n\n--    componentes :: Prop -> [Prop]\n-- tal que (componentes ) es la lista de las componentes de la f\u00f3rmula\n-- f. Por ejemplo, \n--    componentes (p \/\\ q --> r)       ==>  [no (p \/\\ q),r]\n--    componentes (no (p \/\\ q --> r))  ==>  [(p \/\\ q),no r]\n-- ---------------------------------------------------------------------\n\ncomponentes :: Prop -> [Prop]\ncomponentes (Neg (Neg f))    = [f]\ncomponentes (Conj f g)       = [f, g]\ncomponentes (Neg (Impl f g)) = [f, Neg g]\ncomponentes (Neg (Disj f g)) = [Neg f, Neg g]\ncomponentes (Disj f g)       = [f, g]\ncomponentes (Impl f g)       = [Neg f, g]\ncomponentes (Neg (Conj f g)) = [Neg f, Neg g]\ncomponentes (Equi f g)       = [Conj f g, Conj (Neg f) (Neg g)]\ncomponentes (Neg (Equi f g)) = [Conj f (Neg g), Conj (Neg f) g]\n\n-- ---------------------------------------------------------------------\n-- Modelos mediante tableros                                          --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 5: Definir la funci\u00f3n\n--    conjuntoDeLiterales :: [Prop] -> Bool\n-- tal que (conjuntoDeLiterales fs) se verifica si fs es un conjunto de\n-- literales. Por ejemplo, \n--    conjuntoDeLiterales [p --> q, no r, r \/\\ s, p]  ==>  False\n--    conjuntoDeLiterales [p, no q, r]                ==>  True\n-- ---------------------------------------------------------------------\n\nconjuntoDeLiterales :: [Prop] -> Bool\nconjuntoDeLiterales fs =\n    and [literal f | f <- fs]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 6: Definir la funci\u00f3n\n--    tieneContradiccion :: [Prop] -> Bool\n-- tal que (tieneContradiccion fs) se verifica si fs contiene una\n-- f\u00f3rmula y su negaci\u00f3n. Por ejemplo,\n--    tieneContradiccion [r, p \/\\ q, s, no(p \/\\ q)]  ==>  True\n-- ---------------------------------------------------------------------\n\ntieneContradiccion :: [Prop] -> Bool\n-- tieneContradiccion fs \n--     | trace (\"  \" ++ show fs) False = undefined\ntieneContradiccion fs =\n    [f | f <- fs, elem (Neg f) fs] \/= []\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 7: Definir la funci\u00f3n\n--    expansionDN :: [Prop] -> Prop -> [[Prop]]\n-- tal que (expansionDN fs f) es la expansi\u00f3n de fs mediante la doble\n-- negaci\u00f3n f. Por ejemplo,\n--    expansionDN [p, no(no q), r] (no(no q))  ==>  [[q,p,r]]\n-- ---------------------------------------------------------------------\n\nexpansionDN :: [Prop] -> Prop -> [[Prop]]\nexpansionDN fs f =\n    [(componentes f) `union` (delete f fs)]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8: Definir la funci\u00f3n\n--    expansionAlfa :: [Prop] -> Prop -> [[Prop]]\n-- tal que (expansionAlfa fs f) es la expansi\u00f3n de fs mediante la\n-- f\u00f3rmula alfa f. Por ejemplo,\n--    expansionAlfa [q, (p1 \/\\ p2) , r] (p1 \/\\ p2)  ==>  [[p1,p2,q,r]]\n-- ---------------------------------------------------------------------\n\nexpansionAlfa :: [Prop] -> Prop -> [[Prop]]\nexpansionAlfa fs f =\n    [(componentes f) `union` (delete f fs)]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 9: Definir la funci\u00f3n\n--    expansionBeta :: [Prop] -> Prop -> [[Prop]]\n-- tal que (expansionBeta fs f) es la expansi\u00f3n de fs mediante la\n-- f\u00f3rmula beta f. Por ejemplo,\n--    expansionBeta [q, (p1 \\\/ p2) , r] (p1 \\\/ p2)  ==>  [[p1,q,r],[p2,q,r]]\n-- ---------------------------------------------------------------------\n\nexpansionBeta :: [Prop] -> Prop -> [[Prop]]\nexpansionBeta fs f =\n    [[g] `union` (delete f fs) | g <- componentes f]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 10: Definir la funci\u00f3n\n--    sucesores :: [Prop] -> [[Prop]]\n-- tal que (sucesores fs) es la lista de sucesores de fs. Por ejemplo,\n--    sucesores [q \\\/ s, no(no r), p1 \/\\ p2] => [[r,(q \\\/ s),(p1 \/\\ p2)]]\n--    sucesores [r,(q \\\/ s),(p1 \/\\ p2)]      => [[p1,p2,r,(q \\\/ s)]]\n--    sucesores [p1,p2,r,(q \\\/ s)]           => [[q,p1,p2,r],[s,p1,p2,r]]\n-- ---------------------------------------------------------------------\n\nsucesores :: [Prop] -> [[Prop]]\nsucesores fs \n    | doblesNegaci\u00f3n \/= []  = expansionDN   fs (head doblesNegaci\u00f3n)\n    | alfas \/= []           = expansionAlfa fs (head alfas)\n    | betas \/= []           = expansionBeta fs (head betas)\n    where doblesNegaci\u00f3n = [f | f <- fs, dobleNegacion f]\n          alfas          = [f | f <- fs, alfa f]\n          betas          = [f | f <- fs, beta f]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 11: Definir la funci\u00f3n\n--    modelosTab :: [Prop] -> [[Prop]]\n-- tal que (modelosTab fs) es el conjunto de los modelos de fs\n-- calculados mediante el m\u00e9todo de tableros sem\u00e1nticos. Por ejemplo,\n--    modelosTab [p --> q, no(q --> p)]  \n--    ==> [[no p,q],[q,no p]]\n--    modelosTab [p --> q, no q --> no p]  \n--    ==> [[q,no p],[no p],[q],[no p,q]]\n-- ---------------------------------------------------------------------\n\nmodelosTab :: [Prop] -> [[Prop]]\nmodelosTab fs \n    | tieneContradiccion fs  = []\n    | conjuntoDeLiterales fs = [fs]\n    | otherwise              = unionGeneral [modelosTab gs \n                                             | gs <- sucesores fs]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 12: Definir la funci\u00f3n\n--    subconjunto :: Eq a => [a] -> [a] -> Bool\n-- tal que (subconjunto x y) se verifica si x es subconjunto de y. Por\n-- ejemplo, \n--    subconjunto [1,3] [3,2,1]    ==>  True\n--    subconjunto [1,3,5] [3,2,1]  ==> False\n-- ---------------------------------------------------------------------\n\nsubconjunto :: Eq a => [a] -> [a] -> Bool\nsubconjunto xs ys =\n    and [elem x ys | x <- xs]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 13: Definir la funci\u00f3n\n--    modelosGenerales :: [Prop] -> [[Prop]]\n-- tal que (modelosGenerales fs) es el conjunto de los modelos generales\n-- de fs calculados mediante el m\u00e9todo de tableros sem\u00e1nticos. Por\n-- ejemplo, \n--    modelosGenerales [p --> q, no q --> no p]  ==>  [[no p],[q]]\n-- ---------------------------------------------------------------------\n\nmodelosGenerales :: [Prop] -> [[Prop]]\nmodelosGenerales fs =\n    [gs | gs <- modelos\n        , [hs | hs <- delete gs modelos, subconjunto hs gs] == []]\n    where modelos = modelosTab fs\n\n-- ---------------------------------------------------------------------\n-- Teoremas por tableros                                              --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 14: Definir la funci\u00f3n\n--    esTeoremaPorTableros :: Prop -> Bool\n-- tal que (esTeoremaPorTableros f) se verifica si la f\u00f3rmula f es\n-- teorema (mediante tableros sem\u00e1nticos). Por ejemplo,  \n--    esTeoremaPorTableros (p --> p)  ==>  True\n--    esTeoremaPorTableros (p --> q)  ==>  False\n-- ---------------------------------------------------------------------\n\nesTeoremaPorTableros :: Prop -> Bool\nesTeoremaPorTableros f =\n    modelosTab [Neg f] == []\n\n-- ---------------------------------------------------------------------\n-- Consecuencia por tableros                                          --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 15: Definir la funci\u00f3n\n--    esDeduciblePorTableros :: [Prop] -> Prop -> Bool\n-- tal que (esDeduciblePorTableros fs f) se verifica si la f\u00f3rmula f es\n-- consecuencia (mediante tableros) del conjunto de f\u00f3rmulas fs. Por\n-- ejemplo,\n--    esDeduciblePorTableros [p --> q, q --> r] (p --> r)   ==>  True\n--    esDeduciblePorTableros [p --> q, q --> r] (p <--> r)  ==>  False\n-- ---------------------------------------------------------------------\n\nesDeduciblePorTableros :: [Prop] -> Prop -> Bool\nesDeduciblePorTableros fs f =\n    modelosTab ((Neg f):fs) == []\n<\/pre>\n<p>El contenido del m\u00f3dulo SintaxisSemantica es<\/p>\n<pre lang=\"haskell\" title=\"Sintaxis y sem\u00e1ntica proposicional\">\nmodule SintaxisSemantica where\n\n-- ---------------------------------------------------------------------\n-- Librer\u00edas auxiliares                                               --\n-- ---------------------------------------------------------------------\n\nimport Data.List \n\n-- ---------------------------------------------------------------------\n-- Gram\u00e1tica de f\u00f3rmulas prosicionales                                --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 1: Definir los siguientes tipos de datos:\n-- * SimboloProposicional para representar los s\u00edmbolos de proposiciones\n-- * Prop para representar las f\u00f3rmulas proposicionales usando los\n--   constructores Atom, Neg, Conj, Disj, Impl y Equi para las f\u00f3rmulas\n--   at\u00f3micas, negaciones, conjunciones, implicaciones y equivalencias,\n--   respectivamente.  \n-- ---------------------------------------------------------------------\n\ntype SimboloProposicional = String\n\ndata Prop = Atom SimboloProposicional\n          | Neg Prop \n          | Conj Prop Prop \n          | Disj Prop Prop \n          | Impl Prop Prop \n          | Equi Prop Prop \n          deriving (Eq,Ord)\n\ninstance Show Prop where\n    show (Atom p)   = p\n    show (Neg p)    = \"no \" ++ show p\n    show (Conj p q) = \"(\" ++ show p ++ \" \/\\\\ \" ++ show q ++ \")\"\n    show (Disj p q) = \"(\" ++ show p ++ \" \\\\\/ \" ++ show q ++ \")\"\n    show (Impl p q) = \"(\" ++ show p ++ \" --> \" ++ show q ++ \")\"\n    show (Equi p q) = \"(\" ++ show p ++ \" <--> \" ++ show q ++ \")\"\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 2: Definir las siguientes f\u00f3rmulas proposicionales\n-- at\u00f3micas: p, p1, p2, q, r, s, t y u.\n-- ---------------------------------------------------------------------\n\np, p1, p2, q, r, s, t, u :: Prop\np  = Atom \"p\"\np1 = Atom \"p1\"\np2 = Atom \"p2\"\nq  = Atom \"q\"\nr  = Atom \"r\"\ns  = Atom \"s\"\nt  = Atom \"t\"\nu  = Atom \"u\"\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 3: Definir la funci\u00f3n\n--    no :: Prop -> Prop\n-- tal que (no f) es la negaci\u00f3n de f.\n-- ---------------------------------------------------------------------\n\nno :: Prop -> Prop\nno = Neg\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 4: Definir los siguientes operadores\n--    (\/\\), (\\\/), (-->), (<-->) :: Prop -> Prop -> Prop\n-- tales que\n--    f \/\\ g      es la conjunci\u00f3n de f y g\n--    f \\\/ g      es la disyunci\u00f3n de f y g\n--    f --> g     es la implicaci\u00f3n de f a g\n--    f <--> g    es la equivalencia entre f y g\n-- ---------------------------------------------------------------------\n\ninfixr 5 \\\/\ninfixr 4 \/\\\ninfixr 3 -->\ninfixr 2 <-->\n(\/\\), (\\\/), (-->), (<-->) :: Prop -> Prop -> Prop\n(\/\\)   = Conj\n(\\\/)   = Disj\n(-->)  = Impl\n(<-->) = Equi\n\n-- ---------------------------------------------------------------------\n-- S\u00edmbolos proposicionales de una f\u00f3rmula                            --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 5: Definir la funci\u00f3n\n--    simbolosPropForm :: Prop -> [Prop]\n-- tal que (simbolosPropForm f) es el conjunto formado por todos los\n-- s\u00edmbolos proposicionales que aparecen en f. Por ejemplo,\n--    simbolosPropForm (p \/\\ q --> p)  == [p,q]\n-- ---------------------------------------------------------------------\n\nsimbolosPropForm :: Prop -> [Prop]\nsimbolosPropForm (Atom f)   = [(Atom f)]\nsimbolosPropForm (Neg f)    = simbolosPropForm f\nsimbolosPropForm (Conj f g) = simbolosPropForm f `union` simbolosPropForm g\nsimbolosPropForm (Disj f g) = simbolosPropForm f `union` simbolosPropForm g\nsimbolosPropForm (Impl f g) = simbolosPropForm f `union` simbolosPropForm g\nsimbolosPropForm (Equi f g) = simbolosPropForm f `union` simbolosPropForm g\n\n-- ---------------------------------------------------------------------\n-- Interpretaciones                                                   --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 6: Definir el tipo de datos Interpretacion para\n-- representar las interpretaciones como listas de f\u00f3rmulas at\u00f3micas.\n-- ---------------------------------------------------------------------\n\ntype Interpretacion = [Prop]\n\n-- ---------------------------------------------------------------------\n-- Significado de una f\u00f3rmula en una interpretaci\u00f3n                   --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 7: Definir la funci\u00f3n\n--    significado :: Prop -> Interpretacion -> Bool\n-- tal que (significado f i) es el significado de f en i. Por ejemplo,\n--    significado ((p \\\/ q) \/\\ ((no q) \\\/ r)) [r]    ==  False\n--    significado ((p \\\/ q) \/\\ ((no q) \\\/ r)) [p,r]  ==  True\n-- ---------------------------------------------------------------------\n\nsignificado :: Prop -> Interpretacion -> Bool\nsignificado (Atom f)   i = (Atom f) `elem` i\nsignificado (Neg f)    i = not (significado f i)\nsignificado (Conj f g) i = (significado f i) && (significado g i)\nsignificado (Disj f g) i = (significado f i) || (significado g i)\nsignificado (Impl f g) i = significado (Disj (Neg f) g) i\nsignificado (Equi f g) i = significado (Conj (Impl f g) (Impl g f)) i\n\n-- ---------------------------------------------------------------------\n-- Interpretaciones de una f\u00f3rmula                                    --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8: Definir la funci\u00f3n\n--    subconjuntos :: [a] -> [[a]]\n-- tal que (subconjuntos x) es la lista de los subconjuntos de x. Por\n-- ejmplo, \n--    subconjuntos \"abc\"  ==  [\"abc\",\"ab\",\"ac\",\"a\",\"bc\",\"b\",\"c\",\"\"]\n-- ---------------------------------------------------------------------\n\nsubconjuntos :: [a] -> [[a]]\nsubconjuntos []     = [[]]\nsubconjuntos (x:xs) = [x:ys | ys <- xss] ++ xss\n                      where xss = subconjuntos xs\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 9: Definir la funci\u00f3n\n--    interpretacionesForm :: Prop -> [Interpretacion]\n-- tal que (interpretacionesForm f) es la lista de todas las\n-- interpretaciones de f. Por ejemplo, \n--    interpretacionesForm (p \/\\ q --> p)  ==  [[p,q],[p],[q],[]]\n-- ---------------------------------------------------------------------\n\ninterpretacionesForm :: Prop -> [Interpretacion]\ninterpretacionesForm f = subconjuntos (simbolosPropForm f)\n\n-- ---------------------------------------------------------------------\n-- Modelos de f\u00f3rmulas                                                --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 10: Definir la funci\u00f3n\n--    esModeloFormula :: Interpretacion -> Prop -> Bool\n-- tal que (esModeloFormula i f) se verifica si i es un modelo de f. Por\n-- ejemplo, \n--    esModeloFormula [r]   ((p \\\/ q) \/\\ ((no q) \\\/ r))    ==  False\n--    esModeloFormula [p,r] ((p \\\/ q) \/\\ ((no q) \\\/ r))    ==  True\n-- ---------------------------------------------------------------------\n\nesModeloFormula :: Interpretacion -> Prop -> Bool\nesModeloFormula i f = significado f i\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 11: Definir la funci\u00f3n\n--    modelosFormula :: Prop -> [Interpretacion]\n-- tal que (modelosFormula f) es la lista de todas las interpretaciones\n-- de f que son modelo de F. Por ejemplo,\n--    modelosFormula ((p \\\/ q) \/\\ ((no q) \\\/ r)) \n--    == [[p,q,r],[p,r],[p],[q,r]]\n-- ---------------------------------------------------------------------\n\nmodelosFormula :: Prop -> [Interpretacion]\nmodelosFormula f =\n    [i | i <- interpretacionesForm f,\n         esModeloFormula i f]\n\n-- ---------------------------------------------------------------------\n-- F\u00f3rmulas v\u00e1lidas, satisfacibles e insatisfacibles                  --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 12: Definir la funci\u00f3n\n--    esValida :: Prop -> Bool\n-- tal que (esValida f) se verifica si f es v\u00e1lida. Por ejemplo,\n--    esValida (p --> p)                 ==  True\n--    esValida (p --> q)                 ==  False\n--    esValida ((p --> q) \\\/ (q --> p))  ==  True\n-- ---------------------------------------------------------------------\n\nesValida :: Prop -> Bool\nesValida f = \n    modelosFormula f == interpretacionesForm f\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 13: Definir la funci\u00f3n\n--    esInsatisfacible :: Prop -> Bool\n-- tal que (esInsatisfacible f) se verifica si f es insatisfacible. Por\n-- ejemplo, \n--    esInsatisfacible (p \/\\ (no p))             ==  True\n--    esInsatisfacible ((p --> q) \/\\ (q --> r))  ==  False\n-- ---------------------------------------------------------------------\n\nesInsatisfacible :: Prop -> Bool\nesInsatisfacible f =\n    modelosFormula f == []\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 14: Definir la funci\u00f3n\n--    esSatisfacible :: Prop -> Bool\n-- tal que (esSatisfacible f) se verifica si f es satisfacible. Por\n-- ejemplo, \n--    esSatisfacible (p \/\\ (no p))             ==  False\n--    esSatisfacible ((p --> q) \/\\ (q --> r))  ==  True\n-- ---------------------------------------------------------------------\n\nesSatisfacible :: Prop -> Bool\nesSatisfacible f =\n    modelosFormula f \/= []\n\n-- ---------------------------------------------------------------------\n-- S\u00edmbolos proposicionales de un conjunto de f\u00f3rmulas                --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 15: Definir la funci\u00f3n\n--    unionGeneral :: Eq a => [[a]] -> [a]\n-- tal que (unionGeneral x) es la uni\u00f3n de los conjuntos de la lista de\n-- conjuntos x. Por ejemplo,\n--    unionGeneral []                 ==  []\n--    unionGeneral [[1]]              ==  [1]\n--    unionGeneral [[1],[1,2],[2,3]]  ==  [1,2,3]\n-- ---------------------------------------------------------------------\n\nunionGeneral :: Eq a => [[a]] -> [a]\nunionGeneral []     = []\nunionGeneral (x:xs) = x `union` unionGeneral xs \n\n-- ---------------------------------------------------------------------\n-- Ejercicio 16: Definir la funci\u00f3n\n--    simbolosPropConj :: [Prop] -> [Prop]\n-- tal que (simbolosPropConj s) es el conjunto de los s\u00edmbolos\n-- proposiciones de s. Por ejemplo,\n--    simbolosPropConj [p \/\\ q --> r, p --> s]  ==  [p,q,r,s]\n-- ---------------------------------------------------------------------\n\nsimbolosPropConj :: [Prop] -> [Prop]\nsimbolosPropConj s\n    = unionGeneral [simbolosPropForm f | f <- s]\n\n-- ---------------------------------------------------------------------\n-- Interpretaciones de un conjunto de f\u00f3rmulas                        --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 17: Definir la funci\u00f3n\n--    interpretacionesConjunto :: [Prop] -> [Interpretacion]\n-- tal que (interpretacionesConjunto s) es la lista de las\n-- interpretaciones de s. Por ejemplo,\n--    interpretacionesConjunto [p --> q, q --> r]\n--    == [[p,q,r],[p,q],[p,r],[p],[q,r],[q],[r],[]]\n-- ---------------------------------------------------------------------\n\ninterpretacionesConjunto :: [Prop] -> [Interpretacion]\ninterpretacionesConjunto s =\n    subconjuntos (simbolosPropConj s)\n\n-- ---------------------------------------------------------------------\n-- Modelos de conjuntos de f\u00f3rmulas                                   --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 18: Definir la funci\u00f3n\n--    esModeloConjunto :: Interpretacion -> [Prop] -> Bool\n-- tal que (esModeloConjunto i s) se verifica si i es modelo de s. Por\n-- ejemplo, \n--    esModeloConjunto [p,r] [(p \\\/ q) \/\\ ((no q) \\\/ r), q --> r]\n--    == True\n--    esModeloConjunto [p,r] [(p \\\/ q) \/\\ ((no q) \\\/ r), r --> q]\n--    == False\n-- ---------------------------------------------------------------------\n\nesModeloConjunto :: Interpretacion -> [Prop] -> Bool\nesModeloConjunto i s =\n    and [esModeloFormula i f | f <- s]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 19: Definir la funci\u00f3n\n--    modelosConjunto :: [Prop] -> [Interpretacion]\n-- tal que (modelosConjunto s) es la lista de modelos del conjunto\n-- s. Por ejemplo,\n--    modelosConjunto [(p \\\/ q) \/\\ ((no q) \\\/ r), q --> r]\n--    == [[p,q,r],[p,r],[p],[q,r]]\n--    modelosConjunto [(p \\\/ q) \/\\ ((no q) \\\/ r), r --> q]\n--    == [[p,q,r],[p],[q,r]]\n-- ---------------------------------------------------------------------\n\nmodelosConjunto :: [Prop] -> [Interpretacion]\nmodelosConjunto s =\n    [i | i <- interpretacionesConjunto s,\n         esModeloConjunto i s]\n\n-- ---------------------------------------------------------------------\n-- Conjuntos consistentes e inconsistentes de f\u00f3rmulas                --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 20: Definir la funci\u00f3n\n--    esConsistente :: [Prop] -> Bool\n-- tal que (esConsistente s) se verifica si s es consistente. Por\n-- ejemplo, \n--    esConsistente [(p \\\/ q) \/\\ ((no q) \\\/ r), p --> r]        \n--    == True\n--    esConsistente [(p \\\/ q) \/\\ ((no q) \\\/ r), p --> r, no r]  \n--    == False\n-- ---------------------------------------------------------------------\n\nesConsistente :: [Prop] -> Bool\nesConsistente s =\n    modelosConjunto s \/= []\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 21: Definir la funci\u00f3n\n--    esInconsistente :: [Prop] -> Bool\n-- tal que (esInconsistente s) se verifica si s es inconsistente. Por\n-- ejemplo, \n--    esInconsistente [(p \\\/ q) \/\\ ((no q) \\\/ r), p --> r]        \n--    == False\n--    esInconsistente [(p \\\/ q) \/\\ ((no q) \\\/ r), p --> r, no r]  \n--    == True\n-- ---------------------------------------------------------------------\n\nesInconsistente :: [Prop] -> Bool\nesInconsistente s =\n    modelosConjunto s == []\n\n-- ---------------------------------------------------------------------\n-- Consecuencia l\u00f3gica                                                --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 22: Definir la funci\u00f3n\n--    esConsecuencia :: [Prop] -> Prop -> Bool\n-- tal que (esConsecuencia s f) se verifica si f es consecuencia de\n-- s. Por ejemplo,\n--    esConsecuencia [p --> q, q --> r] (p --> r)  ==  True\n--    esConsecuencia [p] (p \/\\ q)                  ==  False\n-- ---------------------------------------------------------------------\n\nesConsecuencia :: [Prop] -> Prop -> Bool\nesConsecuencia s f =\n    null [i | i <- interpretacionesConjunto (f:s),\n              esModeloConjunto i s,\n              not (esModeloFormula i f)]\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. En los ejercicios se usa el m\u00f3dulo SintaxisSemantica desarrollado anteriormente. Las soluciones de los ejercicios se muestran a continuaci\u00f3n.<\/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":[234],"tags":[270,303,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\/4273"}],"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=4273"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4273\/revisions"}],"predecessor-version":[{"id":4276,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4273\/revisions\/4276"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4273"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4273"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4273"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}