Acciones

R2a sol

De Lógica Matemática y fundamentos (2015-16)

Revisión del 12:40 8 mar 2016 de Mjoseh (discusión | contribuciones) (Página creada con '<sourca lang="haskell"> -- SintaxisSemanticaProp.hs -- Lógica proposicional: Sintaxis y semántica -- --------------------------------------------------------------------- mod...')
(dif) ← Revisión anterior | Revisión actual (dif) | Revisión siguiente → (dif)

<sourca lang="haskell"> -- SintaxisSemanticaProp.hs -- Lógica proposicional: Sintaxis y semántica -- ---------------------------------------------------------------------

module SintaxisSemantica where

-- --------------------------------------------------------------------- -- Librerías auxiliares -- -- ---------------------------------------------------------------------

import Data.List

-- --------------------------------------------------------------------- -- Gramática de fórmulas prosicionales -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 1: Definir los siguientes tipos de datos: -- * SímboloProposicional para representar los símbolos de proposiciones -- * Prop para representar las fórmulas proposicionales usando los -- constructores Atom, Neg, Conj, Disj, Impl y Equi para las fórmulas -- atómicas, negaciones, conjunciones, implicaciones y equivalencias, -- respectivamente. -- ---------------------------------------------------------------------

type SímboloProposicional = String

data Prop = Atom SímboloProposicional 

         | Neg Prop 
         | Conj Prop Prop 
         | Disj Prop Prop 
         | Impl Prop Prop 
         | Equi Prop Prop 
         deriving (Eq,Ord)

instance Show Prop where 

   show (Atom p)   = p
   show (Neg p)    = "no " ++ show p
   show (Conj p q) = "(" ++ show p ++ " /\\ " ++ show q ++ ")"
   show (Disj p q) = "(" ++ show p ++ " \\/ " ++ show q ++ ")"
   show (Impl p q) = "(" ++ show p ++ " --> " ++ show q ++ ")"
   show (Equi p q) = "(" ++ show p ++ " <--> " ++ show q ++ ")"

-- --------------------------------------------------------------------- -- Ejercicio 2: Definir las siguientes fórmulas proposicionales -- atómicas: p, p1, p2, q, r, s, t y u. -- ---------------------------------------------------------------------

p, p1, p2, q, r, s, t, u :: Prop p = Atom "p" p1 = Atom "p1" p2 = Atom "p2" q = Atom "q" r = Atom "r" s = Atom "s" t = Atom "t" u = Atom "u"

-- --------------------------------------------------------------------- -- Ejercicio 3: Definir la función -- no :: Prop -> Prop -- tal que (no f) es la negación de f. -- ---------------------------------------------------------------------

no :: Prop -> Prop no = Neg

-- --------------------------------------------------------------------- -- Ejercicio 4: Definir los siguientes operadores -- (/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop -- tales que -- f /\ g es la conjunción de f y g -- f \/ g es la disyunción de f y g -- f --> g es la implicación de f a g -- f <--> g es la equivalencia entre f y g -- ---------------------------------------------------------------------

infixr 5 \/ infixr 4 /\ infixr 3 --> infixr 2 <--> (/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop (/\) = Conj (\/) = Disj (-->) = Impl (<-->) = Equi

-- --------------------------------------------------------------------- -- Símbolos proposicionales de una fórmula -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 5: Definir la función -- símbolosPropFórm :: Prop -> [Prop] -- tal que (símbolosPropFórm f) es el conjunto formado por todos los -- símbolos proposicionales que aparecen en f. Por ejemplo, -- símbolosPropFórm (p /\ q --> p) ==> [p,q] -- ---------------------------------------------------------------------

símbolosPropFórm :: Prop -> [Prop] símbolosPropFórm (Atom f) = [(Atom f)] símbolosPropFórm (Neg f) = símbolosPropFórm f símbolosPropFórm (Conj f g) = símbolosPropFórm f `union` símbolosPropFórm g símbolosPropFórm (Disj f g) = símbolosPropFórm f `union` símbolosPropFórm g símbolosPropFórm (Impl f g) = símbolosPropFórm f `union` símbolosPropFórm g símbolosPropFórm (Equi f g) = símbolosPropFórm f `union` símbolosPropFórm g

-- --------------------------------------------------------------------- -- Interpretaciones -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 6: Definir el tipo de datos Interpretación para -- representar las interpretaciones como listas de fórmulas atómicas. -- ---------------------------------------------------------------------

type Interpretación = [Prop]

-- --------------------------------------------------------------------- -- Significado de una fórmula en una interpretación -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 7: Definir la función -- significado :: Prop -> Interpretación -> Bool -- tal que (significado f i) es el significado de f en i. Por ejemplo, -- significado ((p \/ q) /\ ((no q) \/ r)) [r] ==> False -- significado ((p \/ q) /\ ((no q) \/ r)) [p,r] ==> True -- ---------------------------------------------------------------------

significado :: Prop -> Interpretación -> Bool significado (Atom f) i = (Atom f) `elem` i significado (Neg f) i = not (significado f i) significado (Conj f g) i = (significado f i) && (significado g i) significado (Disj f g) i = (significado f i) || (significado g i) significado (Impl f g) i = significado (Disj (Neg f) g) i significado (Equi f g) i = significado (Conj (Impl f g) (Impl g f)) i

-- --------------------------------------------------------------------- -- Interpretaciones de una fórmula -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 8: Definir la función -- subconjuntos :: [a] -> a -- tal que (subconjuntos x) es la lista de los subconjuntos de x. Por -- ejmplo, -- subconjuntos "abc" ==> ["abc","ab","ac","a","bc","b","c",""] -- ---------------------------------------------------------------------

subconjuntos :: [a] -> a subconjuntos [] = [[]] subconjuntos (x:xs) = [x:ys | ys <- xss] ++ xss 

                     where xss = subconjuntos xs

-- --------------------------------------------------------------------- -- Ejercicio 9: Definir la función -- interpretacionesFórm :: Prop -> [Interpretación] -- tal que (interpretacionesFórm f) es la lista de todas las -- interpretaciones de f. Por ejemplo, -- interpretacionesFórm (p /\ q --> p) ==> [[p,q],[p],[q],[]] -- ---------------------------------------------------------------------

interpretacionesFórm :: Prop -> [Interpretación] interpretacionesFórm f = subconjuntos (símbolosPropFórm f)

-- --------------------------------------------------------------------- -- Modelos de fórmulas -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 10: Definir la función -- esModeloFórmula :: Interpretación -> Prop -> Bool -- tal que (esModeloFórmula i f) se verifica si i es un modelo de f. Por -- ejemplo, -- esModeloFórmula [r] ((p \/ q) /\ ((no q) \/ r)) ==> False -- esModeloFórmula [p,r] ((p \/ q) /\ ((no q) \/ r)) ==> True -- ---------------------------------------------------------------------

esModeloFórmula :: Interpretación -> Prop -> Bool esModeloFórmula i f = significado f i

-- --------------------------------------------------------------------- -- Ejercicio 11: Definir la función -- modelosFórmula :: Prop -> [Interpretación] -- tal que (modelosFórmula f) es la lista de todas las interpretaciones -- de f que son modelo de F. Por ejemplo, -- modelosFórmula ((p \/ q) /\ ((no q) \/ r)) -- ==> [[p,q,r],[p,r],[p],[q,r]] -- ---------------------------------------------------------------------

modelosFórmula :: Prop -> [Interpretación] modelosFórmula f = 

   [i | i <- interpretacionesFórm f,
        esModeloFórmula i f]

-- --------------------------------------------------------------------- -- Fórmulas válidas, satisfacibles e insatisfacibles -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 12: Definir la función -- esVálida :: Prop -> Bool -- tal que (esVálida f) se verifica si f es válida. Por ejemplo, -- esVálida (p --> p) ==> True -- esVálida (p --> q) ==> False -- esVálida ((p --> q) \/ (q --> p)) ==> True -- ---------------------------------------------------------------------

esVálida :: Prop -> Bool esVálida f = 

   modelosFórmula f == interpretacionesFórm f

-- --------------------------------------------------------------------- -- Ejercicio 13: Definir la función -- esInsatisfacible :: Prop -> Bool -- tal que (esInsatisfacible f) se verifica si f es insatisfacible. Por -- ejemplo, -- esInsatisfacible (p /\ (no p)) ==> True -- esInsatisfacible ((p --> q) /\ (q --> r)) ==> False -- ---------------------------------------------------------------------

esInsatisfacible :: Prop -> Bool esInsatisfacible f = 

   modelosFórmula f == []

-- --------------------------------------------------------------------- -- Ejercicio 14: Definir la función -- esSatisfacible :: Prop -> Bool -- tal que (esSatisfacible f) se verifica si f es satisfacible. Por -- ejemplo, -- esSatisfacible (p /\ (no p)) ==> False -- esSatisfacible ((p --> q) /\ (q --> r)) ==> True -- ---------------------------------------------------------------------

esSatisfacible :: Prop -> Bool esSatisfacible f = 

   modelosFórmula f /= []

-- --------------------------------------------------------------------- -- Símbolos proposicionales de un conjunto de fórmulas -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 15: Definir la función -- uniónGeneral :: Eq a => a -> [a] -- tal que (uniónGeneral x) es la unión de los conjuntos de la lista de -- conjuntos x. Por ejemplo, -- uniónGeneral [] ==> [] -- uniónGeneral 1 ==> [1] -- uniónGeneral [[1],[1,2],[2,3]] ==> [1,2,3] -- ---------------------------------------------------------------------

uniónGeneral :: Eq a => a -> [a] uniónGeneral [] = [] uniónGeneral (xs:xss) = xs `union` uniónGeneral xss

uniónG :: Eq a => a -> [a] uniónG = foldl union []


-- --------------------------------------------------------------------- -- Ejercicio 16: Definir la función -- símbolosPropConj :: [Prop] -> [Prop] -- tal que (símbolosPropConj s) es el conjunto de los símbolos -- proposiciones de s. Por ejemplo, -- símbolosPropConj [p /\ q --> r, p --> s] ==> [p,q,r,s] -- ---------------------------------------------------------------------

símbolosPropConj :: [Prop] -> [Prop] símbolosPropConj s 

   = uniónGeneral [símbolosPropFórm f | f <- s]

símbolosPropConj2 :: [Prop] -> [Prop] símbolosPropConj2 = uniónG . map símbolosPropFórm

-- --------------------------------------------------------------------- -- Interpretaciones de un conjunto de fórmulas -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 17: Definir la función -- interpretacionesConjunto :: [Prop] -> [Interpretación] -- tal que (interpretacionesConjunto s) es la lista de las -- interpretaciones de s. Por ejemplo, -- interpretacionesConjunto [p --> q, q --> r] -- ==> [[p,q,r],[p,q],[p,r],[p],[q,r],[q],[r],[]] -- ---------------------------------------------------------------------

interpretacionesConjunto :: [Prop] -> [Interpretación] interpretacionesConjunto s = 

   subconjuntos (símbolosPropConj s)

-- --------------------------------------------------------------------- -- Modelos de conjuntos de fórmulas -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 18: Definir la función -- esModeloConjunto :: Interpretación -> [Prop] -> Bool -- tal que (esModeloConjunto i s) se verifica si i es modelo de s. Por -- ejemplo, -- esModeloConjunto [p,r] [(p \/ q) /\ ((no q) \/ r), q --> r] -- ==> True -- esModeloConjunto [p,r] [(p \/ q) /\ ((no q) \/ r), r --> q] -- ==> False -- ---------------------------------------------------------------------

esModeloConjunto :: Interpretación -> [Prop] -> Bool esModeloConjunto i s = 

   and [esModeloFórmula i f | f <- s]

esModeloConjunto2 :: Interpretación -> [Prop] -> Bool esModeloConjunto2 i s = all (esModeloFórmula i) s

-- --------------------g------------------------------------------------- -- Ejercicio 19: Definir la función -- modelosConjunto :: [Prop] -> [Interpretación] -- tal que (modelosConjunto s) es la lista de modelos del conjunto -- s. Por ejemplo, -- modelosConjunto [(p \/ q) /\ ((no q) \/ r), q --> r] -- ==> [[p,q,r],[p,r],[p],[q,r]] -- modelosConjunto [(p \/ q) /\ ((no q) \/ r), r --> q] -- ==> [[p,q,r],[p],[q,r]] -- ---------------------------------------------------------------------

modelosConjunto :: [Prop] -> [Interpretación] modelosConjunto s = 

   [i | i <- interpretacionesConjunto s,
        esModeloConjunto i s]

-- --------------------------------------------------------------------- -- Conjuntos consistentes e inconsistentes de fórmulas -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 20: Definir la función -- esConsistente :: [Prop] -> Bool -- tal que (esConsistente s) se verifica si s es consistente. Por -- ejemplo, -- esConsistente [(p \/ q) /\ ((no q) \/ r), p --> r] -- ==> True -- esConsistente [(p \/ q) /\ ((no q) \/ r), p --> r, no r] -- ==> False -- ---------------------------------------------------------------------

esConsistente :: [Prop] -> Bool esConsistente s = 

   modelosConjunto s /= []

-- --------------------------------------------------------------------- -- Ejercicio 21: Definir la función -- esInconsistente :: [Prop] -> Bool -- tal que (esInconsistente s) se verifica si s es inconsistente. Por -- ejemplo, -- esInconsistente [(p \/ q) /\ ((no q) \/ r), p --> r] -- ==> False -- esInconsistente [(p \/ q) /\ ((no q) \/ r), p --> r, no r] -- ==> True -- ---------------------------------------------------------------------

esInconsistente :: [Prop] -> Bool esInconsistente s = 

   modelosConjunto s == []

-- --------------------------------------------------------------------- -- Consecuencia lógica -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Ejercicio 22: Definir la función -- esConsecuencia :: [Prop] -> Prop -> Bool -- tal que (esConsecuencia s f) se verifica si f es consecuencia de -- s. Por ejemplo, -- esConsecuencia [p --> q, q --> r] (p --> r) ==> True -- esConsecuencia [p] (p /\ q) ==> False -- ---------------------------------------------------------------------

esConsecuencia :: [Prop] -> Prop -> Bool esConsecuencia s f = 

   null [i | i <- interpretacionesConjunto (f:s),
             esModeloConjunto i s,
             not (esModeloFórmula i f)]

esConsecuencia2 :: [Prop] -> Prop -> Bool esConsecuencia2 s f = 

   and [esModeloFórmula i f | i <- interpretacionesConjunto (f:s),
                              esModeloConjunto i s]

</source>

Obtenido de «https://www.glc.us.es/~jalonso/LMF2016/index.php?title=R2a_sol&oldid=117»