Una solución

-- FormasNormales.hs
-- Formas normales.
-- ---------------------------------------------------------------------

module FormasNormales where

-- ---------------------------------------------------------------------
-- Librería suxiliares                                                --
-- ---------------------------------------------------------------------

import SintaxisSemantica 
import Data.List

-- ---------------------------------------------------------------------
-- Equivalencia lógica                                                --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
--    esEquivalente :: Prop -> Prop -> Bool
-- tal que (esEquivalente f g) se verifica si f y g son
-- equivalentes. Por ejemplo,
--    esEquivalente (p <--> q) ((p --> q) /\ (q --> p))  ==>  True
--    esEquivalente (p --> q)  ((no p) \/ q)             ==>  True
--    esEquivalente (p /\ q)   (no ((no p) \/ (no q)))   ==>  True
--    esEquivalente (p \/ q)   (no ((no p) /\ (no q)))   ==>  True
-- ---------------------------------------------------------------------

esEquivalente :: Prop -> Prop -> Bool
esEquivalente f g = esVálida (Equi f g)

-- ---------------------------------------------------------------------
-- Transformación a forma normal negativa                             --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
--    eliminaEquivalencias :: Prop -> Prop
-- tal que (eliminaEquivalencias f) es una fórmula equivalente a f sin
-- signos de equivalencia. Por ejemplo,
--    eliminaEquivalencias (p <--> q)
--    ==> ((p --> q) /\ (q --> p))
--    eliminaEquivalencias ((p <--> q) /\ (q <--> r))
--    ==> (((p --> q) /\ (q --> p)) /\ ((q --> r) /\ (r --> q)))
-- ---------------------------------------------------------------------

eliminaEquivalencias :: Prop -> Prop
eliminaEquivalencias (Atom f)   = 
    (Atom f)
eliminaEquivalencias (Neg f)    = 
    Neg (eliminaEquivalencias f) 
eliminaEquivalencias (Conj f g) = 
    Conj (eliminaEquivalencias f) (eliminaEquivalencias g) 
eliminaEquivalencias (Disj f g) = 
    Disj (eliminaEquivalencias f) (eliminaEquivalencias g) 
eliminaEquivalencias (Impl f g) = 
    Impl (eliminaEquivalencias f) (eliminaEquivalencias g) 
eliminaEquivalencias (Equi f g) = 
    Conj (Impl (eliminaEquivalencias f) (eliminaEquivalencias g))
         (Impl (eliminaEquivalencias g) (eliminaEquivalencias f))

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
--    eliminaImplicaciones :: Prop -> Prop
-- tal que (eliminaImplicaciones f) es una fórmula equivalente a f sin
-- signos de implicación. Por ejemplo,
--    eliminaImplicaciones (p --> q)
--    ==> (no p \/ q)
--    eliminaImplicaciones (eliminaEquivalencias (p <--> q))
--    ==> ((no p \/ q) /\ (no q \/ p))
-- Nota: Se supone que f no tiene signos de equivalencia.
-- ---------------------------------------------------------------------

eliminaImplicaciones :: Prop -> Prop
eliminaImplicaciones (Atom f)   = 
    (Atom f)
eliminaImplicaciones (Neg f)    = 
    Neg (eliminaImplicaciones f) 
eliminaImplicaciones (Conj f g) = 
    Conj (eliminaImplicaciones f) (eliminaImplicaciones g) 
eliminaImplicaciones (Disj f g) = 
    Disj (eliminaImplicaciones f) (eliminaImplicaciones g) 
eliminaImplicaciones (Impl f g) = 
    Disj (Neg (eliminaImplicaciones f)) (eliminaImplicaciones g) 

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
--    interiorizaNegación :: Prop -> Prop
-- tal que (interiorizaNegación f) es una fórmula equivalente a f donde
-- las negaciones se aplican sólo a fórmulas atómicas. Por ejemplo,
--    interiorizaNegación (no (no p))         ==>  p
--    interiorizaNegación (no (p /\ q))       ==>  (no p \/ no q)
--    interiorizaNegación (no (p \/ q))       ==>  (no p /\ no q)
--    interiorizaNegación (no (no (p \/ q)))  ==>  (p \/ q)
--    interiorizaNegación (no ((no p) \/ q))  ==>  (p /\ no q)
-- Nota: Se supone que f no tiene equivalencias ni implicaciones. 
-- ---------------------------------------------------------------------

interiorizaNegación :: Prop -> Prop
interiorizaNegación (Atom f)   = 
    (Atom f)
interiorizaNegación (Neg f)    = 
    interiorizaNegaciónAux f
interiorizaNegación (Conj f g) = 
    Conj (interiorizaNegación f) (interiorizaNegación g) 
interiorizaNegación (Disj f g) = 
    Disj (interiorizaNegación f) (interiorizaNegación g) 

interiorizaNegaciónAux :: Prop -> Prop
interiorizaNegaciónAux (Atom f)   = 
    Neg (Atom f)
interiorizaNegaciónAux (Neg f)    = 
    interiorizaNegación f 
interiorizaNegaciónAux (Conj f g) = 
    Disj (interiorizaNegaciónAux f) (interiorizaNegaciónAux g) 
interiorizaNegaciónAux (Disj f g) = 
    Conj (interiorizaNegaciónAux f) (interiorizaNegaciónAux g) 


-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
--    formaNormalNegativa :: Prop -> Prop
-- tal que (formaNormalNegativa f) es una fórmula equivalente a f en
-- forma normal negativa. Por ejemplo,
--    formaNormalNegativa (p <--> q)
--    ==> ((no p \/ q) /\ (no q \/ p))
--    formaNormalNegativa ((p \/ (no q)) --> r)
--    ==> ((no p /\ q) \/ r)
--    formaNormalNegativa ((p /\ (q --> r)) --> s)
--    ==> ((no p \/ (q /\ no r)) \/ s)
-- ---------------------------------------------------------------------

formaNormalNegativa :: Prop -> Prop
formaNormalNegativa f =
    interiorizaNegación (eliminaImplicaciones (eliminaEquivalencias f))

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

-- ---------------------------------------------------------------------
-- Ejercicio 6: 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

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir el tipo de dato Literal como sinónimo de
-- fórmula. 
-- ---------------------------------------------------------------------

type Literal = Prop

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
--    complementario :: Literal -> Literal
-- tal que (complementario l) es el complementario de l. Por ejemplo,
--    complementario p       ==>  no p
--    complementario (no p)  ==>  p
-- ---------------------------------------------------------------------

complementario :: Literal -> Literal
complementario (Atom f)       = Neg (Atom f)
complementario (Neg (Atom f)) = Atom f

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
--    literalesFórmulaFNN :: Prop -> [Literal]
-- tal que (literalesFórmulaFNN f) es el conjunto de los literales de la
-- fórmula en forma normal negativa f.
--    literalesFórmulaFNN (p \/ ((no q) \/ r))  ==>  [p,no q,r]
--    literalesFórmulaFNN p                     ==>  [p]
--    literalesFórmulaFNN (no p)                ==>  [no p]
-- ---------------------------------------------------------------------

literalesFórmulaFNN :: Prop -> [Literal]
literalesFórmulaFNN (Disj f g) =
    (literalesFórmulaFNN f) `union` (literalesFórmulaFNN g)
literalesFórmulaFNN (Conj f g) =
    (literalesFórmulaFNN f) `union` (literalesFórmulaFNN g)
literalesFórmulaFNN f          = [f]

-- ---------------------------------------------------------------------
-- Transformación a forma normal conjuntiva                           --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
--    interiorizaDisyunción :: Prop -> Prop
-- tal que (interiorizaDisyunción f) es una fórmula equivalente a f
-- donde las disyunciones sólo se aplica a disyunciones o literales. Por
-- ejemplo,  
--    interiorizaDisyunción (p \/ (q /\ r))  ==>  ((p \/ q) /\ (p \/ r))
--    interiorizaDisyunción ((p /\ q) \/ r)  ==>  ((p \/ r) /\ (q \/ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------

interiorizaDisyunción :: Prop -> Prop
interiorizaDisyunción (Disj (Conj f1 f2) g) =
    interiorizaDisyunción 
    (Conj (Disj (interiorizaDisyunción f1) (interiorizaDisyunción g))
          (Disj (interiorizaDisyunción f2) (interiorizaDisyunción g)))
interiorizaDisyunción (Disj f (Conj g1 g2)) =
    interiorizaDisyunción
    (Conj (Disj (interiorizaDisyunción f) (interiorizaDisyunción g1))
          (Disj (interiorizaDisyunción f) (interiorizaDisyunción g2)))
interiorizaDisyunción (Conj f g) =
    Conj (interiorizaDisyunción f) (interiorizaDisyunción g)
interiorizaDisyunción f = f

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
--    formaNormalConjuntiva :: Prop -> Prop
-- tal que (formaNormalConjuntiva f) es una fórmula equivalente a f en
-- forma normal conjuntiva. Por ejemplo,
--    formaNormalConjuntiva (p /\ (q --> r))
--    ==> (p /\ (no q \/ r))
--    formaNormalConjuntiva (no (p /\ (q --> r)))
--    ==> ((no p \/ q) /\ (no p \/ no r))
--    formaNormalConjuntiva (no(p <--> r))
--    ==> (((p \/ r) /\ (p \/ no p)) /\ ((no r \/ r) /\ (no r \/ no p)))
-- ---------------------------------------------------------------------

formaNormalConjuntiva :: Prop -> Prop
formaNormalConjuntiva f =
    interiorizaDisyunción (formaNormalNegativa f)

-- ---------------------------------------------------------------------

-- Ejercicio 11.2: Definir la función
--    validaPorFNC:: Prop -> Bool
-- tal que (validaPorFNC f) comprueba si f es válida. Por ejemplo,
--    validaPorFNC ((p --> q) \/ (q --> p))    == True
--    validaPorFNC ((p \/ q) /\ ((no q) \/ r)) == False
--    validaPorFNC (p --> p)                   == True
-- ---------------------------------------------------------------------

validaPorFNC:: Prop -> Bool
validaPorFNC f = all tieneParComplementario (listaLiterales f)
    where tieneParComplementario xs = or [(complementario p) `elem` xs | p <- xs]

listaLiterales :: Prop -> [[Prop]]
listaLiterales f = 
    map listaLiteralesDisyuncion 
            (listaDisyuncionesFNC (formaNormalConjuntiva f))

listaDisyuncionesFNC :: Prop -> [Prop]
listaDisyuncionesFNC (Conj f g) = (listaDisyuncionesFNC f) `union`
                                  (listaDisyuncionesFNC g)         
listaDisyuncionesFNC f = [f]

listaLiteralesDisyuncion :: Prop -> [Prop]
listaLiteralesDisyuncion (Disj f g) = (listaLiteralesDisyuncion f) `union`
                                      (listaLiteralesDisyuncion g)
listaLiteralesDisyuncion f = [f]

-- ---------------------------------------------------------------------
-- Transformación a forma normal disyuntiva                           --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
--    interiorizaConjunción :: Prop -> Prop
-- tal que (interiorizaConjunción f) es una fórmula equivalente a f
-- donde las conjunciones sólo se aplica a conjunciones o literales. Por
-- ejemplo,  
--    interiorizaConjunción (p /\ (q \/ r))  ==>  ((p /\ q) \/ (p /\ r))
--    interiorizaConjunción ((p \/ q) /\ r)  ==>  ((p /\ r) \/ (q /\ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------

interiorizaConjunción :: Prop -> Prop
interiorizaConjunción (Conj (Disj f1 f2) g) =
    interiorizaConjunción
    (Disj (Conj (interiorizaConjunción f1) (interiorizaConjunción g))
          (Conj (interiorizaConjunción f2) (interiorizaConjunción g)))
interiorizaConjunción (Conj f (Disj g1 g2)) =
    interiorizaConjunción
    (Disj (Conj (interiorizaConjunción f) (interiorizaConjunción g1))
          (Conj (interiorizaConjunción f) (interiorizaConjunción g2)))
interiorizaConjunción (Disj f g) =
    Disj (interiorizaConjunción f) (interiorizaConjunción g)
interiorizaConjunción f = f

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
--    formaNormalDisyuntiva :: Prop -> Prop
-- tal que (formaNormalDisyuntiva f) es una fórmula equivalente a f en
-- forma normal disyuntiva. Por ejemplo,
--    formaNormalDisyuntiva (p /\ (q --> r))
--    ==> ((p /\ no q) \/ (p /\ r))
--    formaNormalDisyuntiva (no (p /\ (q --> r)))
--    ==> (no p \/ (q /\ no r))
-- ---------------------------------------------------------------------

formaNormalDisyuntiva :: Prop -> Prop
formaNormalDisyuntiva f =
    interiorizaConjunción (formaNormalNegativa f)

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
--     satisfaciblePorFND:: Prop -> Bool
-- tal que (satisfaciblePorFND f) comprueba si f es satisfacible. Por
-- ejemplo,
--     satisfaciblePorFND ((p \/ q) /\ ((no q) \/ r)) == True
--     satisfaciblePorFND (p /\ (no p))               == False
--     satisfaciblePorFND ((p --> q) \/ (q --> p))    == True
-- ---------------------------------------------------------------------

satisfaciblePorFND:: Prop -> Bool
satisfaciblePorFND f = any noTieneParComplementario (listaLiterales' f)
    where noTieneParComplementario xs = 
              and [not ((complementario p) `elem` xs) | p <- xs]

listaLiterales' :: Prop -> [[Prop]]
listaLiterales' f = 
    map listaLiteralesConjuncion 
            (listaConjuncionesFND (formaNormalDisyuntiva f))

listaConjuncionesFND :: Prop -> [Prop]
listaConjuncionesFND (Disj f g) = (listaConjuncionesFND f) `union`
                                  (listaConjuncionesFND g)         
listaConjuncionesFND f = [f]

listaLiteralesConjuncion :: Prop -> [Prop]
listaLiteralesConjuncion (Conj f g) = (listaLiteralesConjuncion f) `union`
                                      (listaLiteralesConjuncion g)
listaLiteralesConjuncion f = [f]