{"id":1963,"date":"2012-03-07T14:19:08","date_gmt":"2012-03-07T14:19:08","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1963"},"modified":"2016-01-09T19:39:29","modified_gmt":"2016-01-09T18:39:29","slug":"lmf2012-ejercicios-de-sintaxis-y-semantica-de-la-logica-proposicional","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2012-ejercicios-de-sintaxis-y-semantica-de-la-logica-proposicional\/","title":{"rendered":"LMF2012: Ejercicios de sintaxis y sem\u00e1ntica de la l\u00f3gica proposicional en Haskell (2)"},"content":{"rendered":"<p>En 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 han comentados las soluciones de los ejercicios de la 2\u00aa relaci\u00f3n, cuyo objetivo es la formalizaci\u00f3n de la sintaxis y la sem\u00e1ntica de la l\u00f3gica proposicional en Haskell.<\/p>\n<p>Las soluciones de los ejercicios corregidos se muestran a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\">\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 han comentados las soluciones de los ejercicios de la 2\u00aa relaci\u00f3n, cuyo objetivo es la formalizaci\u00f3n de la sintaxis y la sem\u00e1ntica de la l\u00f3gica proposicional en Haskell. Las soluciones de los ejercicios corregidos se muestran&#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":[1],"tags":[270,192,156],"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\/1963"}],"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=1963"}],"version-history":[{"count":7,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1963\/revisions"}],"predecessor-version":[{"id":5279,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1963\/revisions\/5279"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1963"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1963"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1963"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}