Relación 7

-- TablerosSemánticos.hs
-- Tableros semánticos proposicionales.
-- José A. Alonso Jiménez <jalonso@us.es>
-- ---------------------------------------------------------------------

module TablerosSemanticos where

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

import SintaxisSemantica
import Data.List 

-- ---------------------------------------------------------------------
-- Literales                                                          --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 0: Definir la función
--    literal :: Prop -> Bool
-- tal que (literal f) se verifica si la fórmula F es un literal. Por
-- ejemplo, 
--    literal p               ==>  True
--    literal (no p)          ==>  True
--    literal (no (p --> q))  ==>  False
-- ---------------------------------------------------------------------

literal :: Prop -> Bool
literal (Atom f) = True
literal (Neg (Atom f)) = True
literal _ = False

-- Jaime Alberto 

literal :: Prop -> Bool
literal (Atom f) = True
literal (Neg f)  = literal f
literal _  = False

-- ---------------------------------------------------------------------
-- Notación uniforme                                                  --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
--    dobleNegación :: Prop -> Bool
-- tal que (dobleNegación f) se verifica si f es una doble negación. Por
-- ejemplo, 
--    dobleNegación (no (no p))     ==>  True
--    dobleNegación (no (p --> q))  ==>  False
-- ---------------------------------------------------------------------

dobleNegación :: Prop -> Bool
dobleNegación (Neg (Neg f)) = True
dobleNegación _ = False

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
--    alfa :: Prop -> Bool
-- tal que (alfa f) se verifica si f es una fórmula alfa.
-- ---------------------------------------------------------------------

alfa :: Prop -> Bool
alfa (Conj f g) = True
alfa (Neg (Disj f g))=True
alfa (Neg(Impl f g))=True
alfa (Equi f g) = True
alfa _ =False
-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
--    beta :: Prop -> Bool
-- tal que (beta d) se verifica si f es una fórmula beta.
-- ---------------------------------------------------------------------

beta :: Prop -> Bool
beta (Disj f g) = True
beta (Neg (Conj f g))=True
beta (Impl f g)=True
beta (Neg (Equi f g)) = True
beta _ =False

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
--    componentes :: Prop -> [Prop]
-- tal que (componentes ) es la lista de las componentes de la fórmula
-- f. Por ejemplo, 
--    componentes (p /\ q --> r)       ==>  [no (p /\ q),r]
--    componentes (no (p /\ q --> r))  ==>  [(p /\ q),no r]
-- ---------------------------------------------------------------------

componentes :: Prop -> [Prop]
componentes (Conj f g)       = [f,g]
componentes (Neg (Impl f g)) = [f, no g]
componentes (Neg (Disj f g)) = [no f, no g]
componentes (Equi f g)       = [no (f-->g), no (g-->f)]


componentes g = [quitanegacion (no x)|x<-componentes (quitanegacion (no g))]
    where quitanegacion (Neg (Neg f)) =f
          quitanegacion f       = f

-- Francisco Javier Carmona

componentes1 :: Prop -> [Prop]
componentes1 (Neg (Neg f)) = [f]
componentes1 (Conj f g) = [f,g]
componentes1 (Neg (Impl f g)) = [f, Neg g]
componentes1 (Neg (Disj f g)) = [Neg f, Neg g]
componentes1 (Equi f g) = [Impl f g, Impl g f]
componentes1 (Disj f g) = [f,g]
componentes1 (Impl f g) = [Neg f, g]
componentes1 (Neg (Conj f g)) = [Neg f, Neg g]
componentes1 (Neg (Equi f g)) = [Neg (Impl f g), Neg (Impl g f)]


-- ---------------------------------------------------------------------
-- Modelos mediante tableros                                          --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
--    conjuntoDeLiterales :: [Prop] -> Bool
-- tal que (conjuntoDeLiterales fs) se verifica si fs es un conjunto de
-- literales. Por ejemplo, 
--    conjuntoDeLiterales [p --> q, no r, r /\ s, p]  ==>  False
--    conjuntoDeLiterales [p, no q, r]                ==>  True
-- ---------------------------------------------------------------------

conjuntoDeLiterales :: [Prop] -> Bool
conjuntoDeLiterales = all (literal)

-- Francisco Javier Carmona

conjuntoDeLiterales1 :: [Prop] -> Bool
conjuntoDeLiterales1 fs = aux fs
                        where aux [] = True
                              aux (x:xs) = literal x && aux xs

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
--    tieneContradicción :: [Prop] -> Bool
-- tal que (tieneContradicción fs) se verifica si fs contiene una
-- fórmula y su negación. Por ejemplo,
--    tieneContradicción [r, p /\ q, s, no(p /\ q)]  ==>  True
-- ---------------------------------------------------------------------

tieneContradicción :: [Prop] -> Bool
tieneContradicción fs = or [elem (no p) fs| p<-fs]
tieneContradicción' fs = or (map (\x-> elem (no x) fs) fs)

tieneContradiccion1 :: [Prop]->Bool
tieneContradiccion1 [] = False
tieneContradiccion1 ((Neg x):xs) = elem x xs || elem (Neg (Neg x)) xs || tieneContradiccion xs
tieneContradiccion1 (x:xs) = elem (Neg x) xs || tieneContradiccion xs

-- Aunque en general tieneContradiccion1 no es más eficiente, sí lo puede ser para 
-- casos puntuales, p.e. ys = [Neg (Atom "q")] ++ [Atom "s" | x <- [1..100000]]++[Atom "q"]


-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
--    expansiónDN :: [Prop] -> Prop -> [[Prop]]
-- tal que (expansiónDN fs f) es la expansión de fs mediante la doble
-- negación f. Por ejemplo,
--    expansiónDN [p, no(no q), r] (no(no q))  ==>  [[q,p,r]]
-- ---------------------------------------------------------------------

expansiónDN :: [Prop] -> Prop -> [[Prop]]
expansiónDN fs (Neg (Neg f)) = [f:(filter (/=Neg(Neg f)) fs)]

-- Francisco Javier Carmona

expansionDN1 :: [Prop] -> Prop -> [[Prop]]
expansionDN1 fs f = [(componentes f) ++ [ x | x <- fs, x /= f]]


-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
--    expansiónAlfa :: [Prop] -> Prop -> [[Prop]]
-- tal que (expansiónAlfa fs f) es la expansión de fs mediante la
-- fórmula alfa f. Por ejemplo,
--    expansiónAlfa [q, (p1 /\ p2) , r] (p1 /\ p2)  ==>  [[p1,p2,q,r]]
-- ---------------------------------------------------------------------

expansiónAlfa :: [Prop] -> Prop -> [[Prop]]
expansiónAlfa fs f = [componentes f++(filter (/=f) fs)]

-- Francisco Javier Carmona

expansionAlfa1 :: [Prop] -> Prop -> [[Prop]]
expansionAlfa1 fs f = [(componentes f) ++ [x | x <- fs, x /= f]]

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
--    expansiónBeta :: [Prop] -> Prop -> [[Prop]]
-- tal que (expansiónBeta fs f) es la expansión de fs mediante la
-- fórmula beta f. Por ejemplo,
--    expansiónBeta [q, (p1 \/ p2) , r] (p1 \/ p2)  ==>  [[p1,q,r],[p2,q,r]]
-- ---------------------------------------------------------------------

expansiónBeta :: [Prop] -> Prop -> [[Prop]]
expansiónBeta fs f = [x:(filter(/=f) fs), y:(filter (/=f) fs)]
                     where x = head (componentes f)
                           y = last (componentes f)

-- Francisco Javier Carmona

expansionBeta1 :: [Prop] -> Prop -> [[Prop]]
expansionBeta1 fs f =  [[head(componentes f)] ++ [x | x <- fs, x /= f],
             [head( reverse(componentes f))] ++ [x | x <- fs, x /= f]]

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
--    sucesores :: [Prop] -> [[Prop]]
-- tal que (sucesores fs) es la lista de sucesores de fs. Por ejemplo,
--    sucesores [q \/ s, no(no r), p1 /\ p2] => [[r,(q \/ s),(p1 /\ p2)]]
--    sucesores [r,(q \/ s),(p1 /\ p2)]      => [[p1,p2,r,(q \/ s)]]
--    sucesores [p1,p2,r,(q \/ s)]           => [[q,p1,p2,r],[s,p1,p2,r]]
-- ---------------------------------------------------------------------

sucesores :: [Prop] -> [[Prop]]
sucesores xs |existeDN xs = expansiónDN xs x
             |existeAlfa xs = expansiónAlfa xs y 
             | otherwise    = expansiónBeta xs z
                              where existeDN xs = or (map
                                                      (dobleNegación) xs)
                                    existeAlfa xs= or (map (alfa) xs)
                                    x= head (filter (dobleNegación) xs)
                                    y= head (filter (alfa) xs)
                                    z= head (filter (beta) xs)

-- Francisco Javier Carmona

sucesores1 :: [Prop] -> [[Prop]]
sucesores1 fs | [] /= haydoble fs = expansionDN fs (head (haydoble fs))
             | [] /= hayalfa fs = expansionAlfa fs (head (hayalfa fs)) 
             | [] /= haybeta fs = expansionBeta fs (head (haybeta fs))
             | otherwise = [[]]

haydoble xs = [ x | x <- xs, dobleNegacion x]

hayalfa ys = [y | y <- ys, alfa y]

haybeta zs = [z | z <- zs, beta z]

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
--    modelosTab :: [Prop] -> [[Prop]]
-- tal que (modelosTab fs) es el conjunto de los modelos de fs
-- calculados mediante el método de tableros semánticos. Por ejemplo,
--    modelosTab [p --> q, no(q --> p)]  
--    ==> [[no p,q],[q,no p]]
--    modelosTab [p --> q, no q --> no p]  
--    ==> [[q,no p],[no p],[q],[no p,q]]
-- ---------------------------------------------------------------------

modelosTab :: [Prop] -> [[Prop]]
modelosTab fs = [x |x<-aux xs, (not.tieneContradicción) x] 

    where aux xs |conjuntoDeLiterales xs = [xs]
                 | otherwise =map (nub) (concat[(modelosTab x)|x<-sucesores xs])

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
--    subconjunto :: Eq a => [a] -> [a] -> Bool
-- tal que (subconjunto x y) se verifica si x es subconjunto de y. Por
-- ejemplo, 
--    subconjunto [1,3] [3,2,1]    ==>  True
--    subconjunto [1,3,5] [3,2,1]  ==> False
-- ---------------------------------------------------------------------

subconjunto :: Eq a => [a] -> [a] -> Bool
subconjunto [] _ = True
subconjunto [x] [y] =False
subconjunto (x:xs) ys |elem x ys = subconjunto xs ys
                      | otherwise=False

-- Francisco Javier Carmona

subconjunto1 :: Eq a => [a] -> [a] -> Bool
subconjunto1 xs ys = length xs == length [x | x <- xs, elem x ys]

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
--    modelosGenerales :: [Prop] -> [[Prop]]
-- tal que (modelosGenerales fs) es el conjunto de los modelos generales
-- de fs calculados mediante el método de tableros semánticos. Por
-- ejemplo, 
--    modelosGenerales [p --> q, no q --> no p]  ==>  [[no p],[q]]
-- ---------------------------------------------------------------------

modelosGenerales :: [Prop] -> [[Prop]]
modelosGenerales fs =  aux ps (modelosTab fs)
    where aux [] ys = ys 
          aux (x:xs) ys = aux xs (delete x ys)
          ps  = [x |x<-modelosTab fs, f x (modelosTab fs)]
          f x xs = or [ subconjunto y x|y<-xs,x/=y]


modelosGenerales1 :: [Prop] -> [[Prop]]
modelosGenerales1 xs = limpieza (modelosTab xs)
limpieza [] = []
limpieza (x:xs) | or [subconjunto x y | y <- xs] = limpieza xs
                | otherwise = x:limpieza [y | y <- xs, not(subconjunto y
                                                                       x)]

-- ---------------------------------------------------------------------
-- Teoremas por tableros                                              --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
--    esTeoremaPorTableros :: Prop -> Bool
-- tal que (esTeoremaPorTableros f) se verifica si la fórmula f es
-- teorema (mediante tableros semánticos). Por ejemplo,  
--    esTeoremaPorTableros (p --> p)  ==>  True
--    esTeoremaPorTableros (p --> q)  ==>  False
-- ---------------------------------------------------------------------

esTeoremaPorTableros :: Prop -> Bool
esTeoremaPorTableros f = null (modelosTab [no f])

-- Francisco Javier Carmona 

esTeoremaPorTableros1 :: Prop -> Bool
esTeoremaPorTableros1 f = modelosTab [Neg f] == [] 


-- ---------------------------------------------------------------------
-- Consecuencia por tableros                                          --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
--    esDeduciblePorTableros :: [Prop] -> Prop -> Bool
-- tal que (esDeduciblePorTableros fs f) se verifica si la fórmula f es
-- consecuencia (mediante tableros) del conjunto de fórmulas fs. Por
-- ejemplo,
--    esDeduciblePorTableros [p --> q, q --> r] (p --> r)   ==>  True
--    esDeduciblePorTableros [p --> q, q --> r] (p <--> r)  ==>  False
-- ---------------------------------------------------------------------

esDeduciblePorTableros :: [Prop] -> Prop -> Bool
esDeduciblePorTableros fs f = null (modelosGenerales (no f:fs))

-- Francisco Javier Carmona

esDeduciblePorTableros1 :: [Prop] -> Prop -> Bool
esDeduciblePorTableros1 fs f = modelosTab ((Neg f):fs) == []