Ver el código de «Ejercicio 4 (a)» - Lógica matemática y fundamentos (2014-15)

<source lang="haskell">

-- ---------------------------------------------------------------------
-- 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]
</pre>