Relación 8

-- 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
-- ---------------------------------------------------------------------
-- "Pedro Ros"
literal :: Prop -> Bool
literal (Atom p) = True
literal (Neg (Atom p)) = True
literal x = 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
-- ---------------------------------------------------------------------
-- Pedro Ros
dobleNegacion :: Prop -> Bool
dobleNegacion (Neg (Neg p))= True
dobleNegacion x = False
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
--    alfa :: Prop -> Bool
-- tal que (alfa f) se verifica si f es una fórmula alfa.
-- ---------------------------------------------------------------------
-- Pedro Ros
alfa :: Prop -> Bool
alfa (Conj p q) = True
alfa (Neg (Impl p q))= True
alfa (Neg (Disj p q))= True
alfa (Equi p q) = True
alfa x = False

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
--    beta :: Prop -> Bool
-- tal que (beta d) se verifica si f es una fórmula beta.
-- ---------------------------------------------------------------------
-- Pedro Ros
beta :: Prop -> Bool
beta (Disj p q) = True
beta (Impl p q) = True
beta (Neg (Conj p q)) = True
beta (Neg (Equi p q))= True
beta p = 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]
-- ---------------------------------------------------------------------
-- Pedro Ros
componentes :: Prop -> [Prop]
componentes (Conj p q) = [p,q]
componentes (Neg(Impl p q)) = [p,no q]
componentes (Neg(Disj p q))= [no p, no q]
componentes (Equi p q) = [Impl p q, Impl q p]
componentes (Disj p q) = [p, q]
componentes (Impl p q) = [no p, q]
componentes (Neg(Conj p q))= [no p, no q]
componentes (Neg(Equi p q))=[Neg(Impl p q), Neg(Impl q p)]
 
-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro Ros
conjuntoDeLiterales :: [Prop] -> Bool
conjuntoDeLiterales []= True
conjuntoDeLiterales (x:xs)= if literal x then conjuntoDeLiterales xs
                            else False

-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
-- Pedro Ros
tieneContradiccion :: [Prop] -> Bool
tieneContradiccion [f] = False
tieneContradiccion ((Neg f):fs) = if elem f fs then True else
                                      tieneContradiccion fs
tieneContradiccion (f:fs)= if elem (no f) fs then True else
                               tieneContradiccion fs



-- Isabel Duarte
tieneContradiccion2 :: [Prop] -> Bool
tieneContradiccion2 fs = or [elem (no x) fs | x <- fs]


-- ---------------------------------------------------------------------
-- 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]]
-- ---------------------------------------------------------------------
--José María Contreras
elim (Neg(Neg f)) = f 
                        
                        
expansionDN :: [Prop] -> Prop -> [[Prop]]
expansionDN fs f = [(elim 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]]
-- ---------------------------------------------------------------------
--José María Contreras

expansionAlfa :: [Prop] -> Prop -> [[Prop]]
expansionAlfa fs f = [(componentes f)`union`(delete f fs)]


-- ---------------------------------------------------------------------
-- 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]]
-- ---------------------------------------------------------------------
--José María Contreras

expansionBeta :: [Prop] -> Prop -> [[Prop]]
expansionBeta fs f = [x:(delete f fs)| x<-(componentes 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]]
-- ---------------------------------------------------------------------
-- Pedro Ros
sucesores :: [Prop] -> [[Prop]]
sucesores fs |[f|f<-fs, dobleNegacion f]/=[] = expansionDN fs (head([f|f<-fs,dobleNegacion f]))
             |[f|f<-fs, alfa f]/=[] =expansionAlfa fs (head([f|f<-fs,alfa f]))
             |[f|f<-fs, beta f]/=[] =expansionBeta fs (head([f|f<-fs,beta f]))
             |otherwise = [fs]

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

-- Pedro Ros
modelosTab :: [Prop] -> [[Prop]]
modelosTab fs |[f|f<-fs, not(literal f)]/=[] = concat [modelosTab (nub x) | x<-(sucesores fs)]
              |otherwise = [fs]

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

-- Isabel Duarte
subconjunto :: Eq a => [a] -> [a] -> Bool
subconjunto xs ys = and [elem x ys | x <- xs]


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

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

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