Ejercicio 4 (a)

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

-- --------------------------------------------------------------------- -- Se definen los siguientes tipos de datos: -- * SimboloProposicional 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 SimboloProposicional = String

data Prop = Atom SimboloProposicional

         | 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 ++ ")"

-- --------------------------------------------------------------------- -- Se definen 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"

-- --------------------------------------------------------------------- -- Se define la función -- no :: Prop -> Prop -- tal que (no f) es la negación de f. -- ---------------------------------------------------------------------

no :: Prop -> Prop no = Neg

-- --------------------------------------------------------------------- -- Se definen 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

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

-- --------------------------------------------------------------------- -- Se define el tipo de datos Interpretación para representar las -- interpretaciones como listas de pares (átomo,booleano). -- ---------------------------------------------------------------------

type Interpretacion = [(Prop,Bool)]

-- --------------------------------------------------------------------- -- Se define el tipo de dato Literal como sinónimo de fórmula. -- ---------------------------------------------------------------------

type Literal = Prop

-- --------------------------------------------------------------------- -- Cláusulas -- -- ---------------------------------------------------------------------

-- --------------------------------------------------------------------- -- Se define el tipo de datos Cláusula como una lista de literales. -- ---------------------------------------------------------------------

type Clausula = [Literal]

-- --------------------------------------------------------------------- -- Ejercicio 4. Definir la función -- esModeloClausula :: Interpretacion -> Cláusula -> Bool -- tal que (esModeloClausula i c) se verifica si i es modelo de c . Por -- ejemplo, -- esModeloClausula [(p,True),(q,False),(r,True)] [p, q] == True -- esModeloClausula [(p,False),(q,False),(r,True)] [p, no q] == True -- esModeloClausula [(p,False),(q,True),(r,True)] [p, no q] == False -- esModeloClausula [(p,False),(q,True),(r,True)] [] == False -- esModeloClausula [(p,False),(q,True),(r,True)] [no q] == False -- esModeloClausula [(p,False),(q,False),(r,True)] [no q] == True -- ---------------------------------------------------------------------

esModeloClausula :: Interpretacion -> Clausula -> Bool esModeloClausula i c = or [esModeloLiteral i l | l <- c]

esModeloLiteral :: Interpretacion -> Literal -> Bool esModeloLiteral i (Atom s) = busca (Atom s) i esModeloLiteral i (Neg (Atom s)) = not (esModeloLiteral i (Atom s))

busca :: Eq t1 => t1 -> [(t1, t)] -> t busca p i = head [v | (a,v) <- i, a == p]

De Lógica matemática y fundamentos (2014-15)