-- FormasNormales.hs
-- Formas normales.
-- ---------------------------------------------------------------------
module FormasNormales where
-- ---------------------------------------------------------------------
-- Librería suxiliares --
-- ---------------------------------------------------------------------
import SintaxisSemantica
import Data.List
-- ---------------------------------------------------------------------
-- Equivalencia lógica --
-- ---------------------------------------------------------------------
-- Pedro Ros
esEquivalente :: Prop -> Prop -> Bool
esEquivalente f g = null[n|n<-modelosFormula f,not(esModeloFormula n g)]
-- Es necesario que cambiéis cosas de la Rel2.hs
-- ---------------------------------------------------------------------
-- 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)))
-- ---------------------------------------------------------------------
-- Pedro Ros
eliminaEquivalencias :: Prop -> Prop
eliminaEquivalencias (Equi a b)= Conj (Impl a b) (Impl b a)
eliminaEquivalencias (Disj a b)= Disj (eliminaEquivalencias a)
(eliminaEquivalencias b)
eliminaEquivalencias (Conj a b) = Conj (eliminaEquivalencias a)
(eliminaEquivalencias b)
eliminaEquivalencias (Impl a b)= Impl (eliminaEquivalencias a)
(eliminaEquivalencias b)
eliminaEquivalencias (Neg a) = Neg (eliminaEquivalencias a)
eliminaEquivalencias (Atom p) = Atom p
-- ---------------------------------------------------------------------
-- 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.
-- ---------------------------------------------------------------------
-- Pedro Ros
eliminaImplicaciones :: Prop -> Prop
eliminaImplicaciones (Impl a b)= Disj (Neg (eliminaImplicaciones a))
(eliminaImplicaciones b)
eliminaImplicaciones (Disj a b)= Disj (eliminaImplicaciones a)
(eliminaImplicaciones b)
eliminaImplicaciones (Conj a b) = Conj (eliminaImplicaciones a)
(eliminaImplicaciones b)
eliminaImplicaciones (Neg a) = Neg (eliminaImplicaciones a)
eliminaImplicaciones (Atom p) = Atom p
-- ---------------------------------------------------------------------
-- 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.
-- ---------------------------------------------------------------------
-- Pedro Ros
interiorizaNegacion :: Prop -> Prop
interiorizaNegacion (Neg (Conj a b))=(Disj (interiorizaNegacion(no (interiorizaNegacion a)))
(interiorizaNegacion(no (interiorizaNegacion b))))
interiorizaNegacion (Neg (Disj a b))=(Conj (interiorizaNegacion(no (interiorizaNegacion a)))
(interiorizaNegacion(no (interiorizaNegacion b))))
interiorizaNegacion (Neg (Neg f))= (interiorizaNegacion f)
interiorizaNegacion (Disj a b)= Disj (interiorizaNegacion a)
(interiorizaNegacion b)
interiorizaNegacion (Conj a b)= Conj (interiorizaNegacion a)
(interiorizaNegacion b)
interiorizaNegacion x = x
-- ---------------------------------------------------------------------
-- 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)
-- ---------------------------------------------------------------------
-- Pedro Ros
formaNormalNegativa :: Prop -> Prop
formaNormalNegativa =interiorizaNegacion.eliminaImplicaciones.eliminaEquivalencias
-- ---------------------------------------------------------------------
-- 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
-- ---------------------------------------------------------------------
--Isabel Duarte
literal :: Prop -> Bool
literal (Atom p) = True
literal (Neg (Atom p)) = 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
-- ---------------------------------------------------------------------
--Isabel Duarte
complementario :: Literal -> Literal
complementario (Atom p) = Neg (Atom p)
complementario (Neg (Atom p)) = Atom p
-- ---------------------------------------------------------------------
-- 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]
-- ---------------------------------------------------------------------
--Isabel Duarte
literalesFormulaFNN :: Prop -> [Literal]
literalesFormulaFNN (Conj p q) =
union (literalesFormulaFNN p) (literalesFormulaFNN q)
literalesFormulaFNN (Disj p q) =
union (literalesFormulaFNN p) (literalesFormulaFNN q)
literalesFormulaFNN p = [p]
-- ---------------------------------------------------------------------
-- 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.
-- ---------------------------------------------------------------------
--Isabel Duarte
interiorizaDisyuncion :: Prop -> Prop
interiorizaDisyuncion (Disj (Conj p q) r) =
interiorizaDisyuncion
(Conj (Disj (interiorizaDisyuncion p) (interiorizaDisyuncion r))
(Disj (interiorizaDisyuncion q) (interiorizaDisyuncion r)))
interiorizaDisyuncion (Disj r (Conj p q)) =
interiorizaDisyuncion
(Conj (Disj (interiorizaDisyuncion r) (interiorizaDisyuncion p))
(Disj (interiorizaDisyuncion r) (interiorizaDisyuncion q)))
interiorizaDisyuncion (Conj p q) =
Conj (interiorizaDisyuncion p) (interiorizaDisyuncion q)
interiorizaDisyuncion 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)))
-- ---------------------------------------------------------------------
--Isabel Duarte
formaNormalConjuntiva :: Prop -> Prop
formaNormalConjuntiva f = interiorizaDisyuncion (formaNormalNegativa f)
-- ---------------------------------------------------------------------
-- Ejercicio 11.2: validaPorFNC
validaPorFNC:: Prop -> Bool
validaPorFNC = undefined
-- validaPorFNC ((p --> q) \/ (q --> p)) == True
-- validaPorFNC ((p \/ q) /\ ((no q) \/ r)) == False
-- validaPorFNC (p --> p) == True
-- ---------------------------------------------------------------------
-- 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.
-- ---------------------------------------------------------------------
--Isabel Duarte
interiorizaConjuncion :: Prop -> Prop
interiorizaConjuncion (Conj (Disj f g) h) =
interiorizaConjuncion (Disj (Conj (interiorizaConjuncion f) (interiorizaConjuncion h))
(Conj (interiorizaConjuncion g) (interiorizaConjuncion h)))
interiorizaConjuncion (Conj f (Disj g h)) =
interiorizaConjuncion (Disj (Conj (interiorizaConjuncion f) (interiorizaConjuncion g))
(Conj (interiorizaConjuncion f) (interiorizaConjuncion h)))
interiorizaConjuncion (Disj f g) =
Disj (interiorizaConjuncion f) (interiorizaConjuncion g)
interiorizaConjuncion 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))
-- ---------------------------------------------------------------------
--Isabel Duarte
formaNormalDisyuntiva :: Prop -> Prop
formaNormalDisyuntiva f = interiorizaConjuncion (formaNormalNegativa f)
-- ---------------------------------------------------------------------
-- Ejercicio 13.2: satisfaciblePorFND
satisfaciblePorFND:: Prop -> Bool
satisfaciblePorFND f = undefined
-- satisfaciblePorFND ((p \/ q) /\ ((no q) \/ r)) == True
-- satisfaciblePorFND (p /\ (no p)) == False
-- satisfaciblePorFND ((p --> q) \/ (q --> p)) == True
