Ejercicio 4 (b)

-- ---------------------------------------------------------------------
-- 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 fórmulas atómicas. 
-- ---------------------------------------------------------------------

type Interpretacion = [Prop]


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

-- ---------------------------------------------------------------------
-- Definimos el tipo de datos Cláusula c como una par (pos, neg), donde
-- pos es la lista de los átomos correspondientes a los literales
-- positivos de c y neg la lista de los átomos correspondientes a los
-- literales negativos de c.
-- ---------------------------------------------------------------------

type Clausula = ([Prop],[Prop])

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

esModeloAtom :: Interpretacion -> Prop -> Bool
esModeloAtom i (Atom s) = elem (Atom s) i

esModeloClausula :: Interpretacion -> Clausula -> Bool
esModeloClausula i (pos,neg) 
    | null pos && null neg = False
    | otherwise            = or [esModeloAtom i a | a <- pos] || 
                             or [not (esModeloAtom i a) | a <-neg]

-- O bien:
esModeloClausula' :: Interpretacion -> Clausula -> Bool
esModeloClausula' i (pos,neg) = 
    or [elem x i | x <-pos] || or [notElem x i | x <- neg]
De Lógica matemática y fundamentos (2014-15)
