Relación 2a

-- SintaxisSemanticaProp.hs
-- Lógica proposicional: Sintaxis y semántica
-- José A. Alonso Jiménez <jalonso@us.es>
-- ---------------------------------------------------------------------

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


simbolosPropForm :: Prop -> [Prop]
simbolosPropForm (Atom p) = [Atom p]
simbolosPropForm (Neg p) = simbolosPropForm p
simbolosPropForm (Conj p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))
simbolosPropForm (Disj p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))
simbolosPropForm (Impl p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))
simbolosPropForm (Equi p q) = nub ((simbolosPropForm p) ++ (simbolosPropForm q))

-- Luis Curquejo

-- Comentario: La definición se puede mejorar usando la función union.


-- ---------------------------------------------------------------------
-- 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 -> Interpretacion -> Bool
significado (Atom f) xs | elem (Atom f) xs = True
                        | otherwise = False
significado (Neg f) xs = not (significado f xs)
significado (Conj f q) xs = (significado f xs) && (significado q xs)
significado (Disj f q) xs = (significado f xs) || (significado q xs)
significado (Impl f q) xs | (significado f xs) == True = significado q xs
                          | otherwise = True
significado (Equi f q) xs = (significado f xs) == (significado q xs)

--Luis Curquejo

-- Comentario: la definición se puede simplificar.

significado :: Prop -> Interpretacion -> Bool
significado (Atom p) i = elem (Atom p) i
significado (Neg p) i = not (significado p i)
significado (Conj p q) i = (significado p i)&&(significado q i)
significado (Disj p q) i = (significado p i)||(significado q i)
significado (Impl p q) i | significado p i = significado q i
                         | otherwise = True
significado (Equi p q) i = (significado p i)==(significado q i)

--María Dolores Mateo Ceballos



significado (Impl p q) i = (significado p i) <= (significado q i)

--Nikola Drousie (el resto sería igual que María Dolores)

-- ---------------------------------------------------------------------
-- 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 [a] = [[],[a]]
subconjuntos (x:xs) = [x:ys  | ys <- sub] ++ sub
                      where sub = subconjuntos xs
-- Me acordaba de primero (seguro) Javier Rodríguez Vivas
-- Jaime Alberto

subconjuntos :: [a] -> [[a]]
subconjuntos [] = [[]]
subconjuntos (x:xs) = [x:ys | ys<-subconjuntos xs] ++ 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],[]]
-- ---------------------------------------------------------------------

interpretacionesForm :: Prop -> [Interpretacion]
interpretacionesForm f = subconjuntos (simbolosPropForm f)

--Luis Curquejo

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

esModeloFormula :: Interpretacion -> Prop -> Bool
esModeloFormula i f = significado f i

-- Luis Curquejo
-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 <- subconjuntos (símbolosPropFórm f), esModeloFórmula i f]

-- Elisa Mazuelos Jiménez

-- Comentario: la definición se puede simplificar usando interpretacionesForm.

modelosFormula :: Prop -> [Interpretacion]
modelosFormula f = [xs|xs<-(interpretacionesForm f), esModeloFormula xs f]

--María Dolores Mateo Ceballos

modelosFormula :: Prop -> [Interpretacion]
modelosFormula f = aux (interpretacionesForm f)
                   where aux [] = []
                         aux (x:xs) | esModeloFormula x f = x : aux xs
                                    | otherwise = aux xs

-- Francisco Javier Carmona

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

esValida :: Prop -> Bool
esValida f = subconjuntos (simPro f) == modelosFormula f 

-- Javier Rodríguez Vivas

-- Comentario: la definición se puede simplificar usando interpretacionesForm.
 
esValida :: Prop -> Bool
esValida f = modelosFormula f == interpretacionesForm f

-- María Dolores Mateo Ceballos 
-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = null (modelosFórmula f)
--Emilio Martinez Rivero


esInsatisfacible :: Prop -> Bool
esInsatisfacible f = modelosFormula f == []

-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = not . EsInsatisfacible
--Emilio Martinez Rivero


esSatisfacible :: Prop -> Bool
esSatisfacible f = modelosFormula f /= []

-- Francisco Javier Carmona

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

unionGeneral :: Eq a => [[a]] -> [a]
unionGeneral [] = []
unionGeneral (x:xs) = nub(x++ unionGeneral xs)

--Javier Rodríguez Vivas
-- Francisco Javier Carmona

-- Comentario: La definición se puede mejorar usando la función union.

uniónGeneral :: Eq a => [[a]] -> [a]
uniónGeneral = nub . concat

-- Elisa Mazuelos Jiménez




unionGeneral :: Eq a => [[a]] -> [a]
unionGeneral [] = []
unionGeneral (xs:xss) = union xs (unionGeneral xss)

-- Maria del Carmen Mesa Marquez 


-- ---------------------------------------------------------------------
-- 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 [simb x | x<-s]

--Emilio Martinez Rivero

simbolosPropConj :: [Prop] -> [Prop]
simbolosPropConj s = nub (aux s)
                    where aux [] = []
                          aux (x:xs) = simbolosPropForm x ++
                                       simbolosPropConj xs

-- Francisco Javier Carmona

simbolosPropConj :: [Prop] -> [Prop]
simbolosPropConj s = unionGeneral (map simbolosPropForm s)

-- Luis Palma Blanco

-- ---------------------------------------------------------------------
-- 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 = subconjuntos . símbolosPropConj

-- Elisa Mazuelos Jiménez

-- ---------------------------------------------------------------------
-- 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 = elem False xs == False
   where xs = [esModeloFormula i f | f<-s]

--Javier Rodriguez Vivas

-- Comentario: la definición se puede mejorar.

esModeloConjunto :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i s = and [esModeloFormula i f| f<-s]

--María Dolores Mateo Ceballos

esModeloConjunto :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i s = aux i s
                      where aux i []  = True
                            aux i  (x:xs)  = esModeloFormula i x && 
                                              esModeloConjunto i xs

-- Francisco Javier Carmona

-- Jaime Alberto
esModeloConjunto :: Interpretacion -> [Prop] -> Bool
esModeloConjunto i [f] = esModeloFormula i f
esModeloConjunto i (x:xs) | esModeloFormula i x = esModeloConjunto i xs
                          | otherwise = False 

-- ---------------------------------------------------------------------
-- 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 = [x|x<-interpretacionesConjunto s, esModeloConjunto x s]
--Emilio Martinez Rivero
-- ---------------------------------------------------------------------
-- 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 = or [esModeloConjunto x s | x <- (modelosConjunto s)]

-- Elisa Mazuelos Jiménez

-- Comentario: La definición se puede mejorar.

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

-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = not . esConsistente

-- Elisa Mazuelos Jiménez

esInconsistente :: [Prop] -> Bool
esInconsistente s = null (modelosConjunto s)

-- María Dolores Mateo Ceballos

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

-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- 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 = and [esModeloFórmula x f| x<-modelosConjunto s]

--Emilio Martinez Rivero

-- Comentario: la definición no es correcta.

esConsecuencia :: [Prop] -> Prop -> Bool
esConsecuencia s f = esInconsistente ((no f):s)

--María Dolores Mateo Ceballos

esConsecuencia :: [Prop] -> Prop -> Bool
esConsecuencia s f = or [elem x (modelosConjunto s)| x<-(modelosFormula f)]

-- Luis Palma Blanco