-- Clausulas.hs
-- Cláusulas.
-- ---------------------------------------------------------------------
module Clausulas where
-- ---------------------------------------------------------------------
-- Librería suxiliares --
-- ---------------------------------------------------------------------
import SintaxisSemantica
import FormasNormales
import Data.List
-- ---------------------------------------------------------------------
-- Cláusulas --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir el tipo de datos Clausula como una lista de
-- literales.
-- ---------------------------------------------------------------------
type Clausula = [Literal]
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- clausula :: Prop -> Clausula
-- tal que (clausula f) es la clausula de la fórmula-clausal f. Por
-- ejemplo,
-- clausula p ==> [p]
-- clausula (no p) ==> [no p]
-- clausula (((no p) \/ r) \/ ((no p) \/ q)) ==> [q,r,no p]
-- ---------------------------------------------------------------------
clausula :: Prop -> Clausula
clausula f
| literal f = [f]
clausula (Disj f g) = sort ((clausula f) `union` (clausula g))
-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- clausulasFNC :: Prop -> [Clausula]
-- tal que (clausulasFNC f) es el conjunto de clausulas de la fórmula en
-- forma normal conjuntiva f. Por ejmplo,
-- clausulasFNC (p /\ ((no q) \/ r))
-- ==> [[p],[r, no q]]
-- clausulasFNC (((no p) \/ q) /\ ((no p) \/ (no r)))
-- ==> [[q, no p],[no p,no r]]
-- ---------------------------------------------------------------------
clausulasFNC :: Prop -> [Clausula]
clausulasFNC (Conj f g) =
(clausulasFNC f) `union` (clausulasFNC g)
clausulasFNC f =
[clausula f]
-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- clausulas :: Prop -> [Clausula]
-- tal que (clausulas f) es un conjunto de clausulas equivalente a
-- f. Por ejemplo,
-- clausulas (p /\ (q --> r))
-- ==> [[p],[r,no q]]
-- clausulas (no (p /\ (q --> r)))
-- ==> [[q,no p],[no p,no r]]
-- clausulas (no(p <--> r))
-- ==> [[p,r],[p,no p],[r,no r],[no p,no r]]
-- ---------------------------------------------------------------------
clausulas :: Prop -> [Clausula]
clausulas f =
clausulasFNC (formaNormalConjuntiva f)
-- ---------------------------------------------------------------------
-- Clausulas de un conjunto de fórmulas --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- clausulasConjunto :: [Prop] -> [Clausula]
-- tal que (clausulasConjunto s) es un conjunto de clausulas equivalente
-- a s. Por ejemplo,
-- clausulasConjunto [p --> q, q --> r] ==> [[q,no p],[r,no q]]
-- clausulasConjunto [p --> q, q <--> p] ==> [[q,no p],[p,no q]]
-- ---------------------------------------------------------------------
clausulasConjunto :: [Prop] -> [Clausula]
clausulasConjunto s =
unionGeneral [clausulas f | f <- s]
-- ---------------------------------------------------------------------
-- Simbolos proposicionales de una clausula --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- simbolosProposicionalesClausula :: Clausula -> [Prop]
-- tal que (simbolosProposicionalesClausula c) es el conjunto de los
-- simbolos proposicionales de c. Por ejemplo,
-- simbolosProposicionalesClausula [p, q, no p] ==> [p,q]
-- ---------------------------------------------------------------------
simbolosProposicionalesClausula :: Clausula -> [Prop]
simbolosProposicionalesClausula = simbolosPropConj
-- ---------------------------------------------------------------------
-- Simbolos proposicionales de un conjunto de clausulas --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
-- simbolosProposicionalesConjuntoClausula :: [Clausula] -> [Prop]
-- tal que (simbolosProposicionalesConjuntoClausula s) es el conjunto de los
-- simbolos proposicionales de s. Por ejemplo,
-- simbolosProposicionalesConjuntoClausula [[p, q],[no q, r]]
-- ==> [p,q,r]
-- ---------------------------------------------------------------------
simbolosProposicionalesConjuntoClausula :: [Clausula] -> [Prop]
simbolosProposicionalesConjuntoClausula s =
unionGeneral [simbolosProposicionalesClausula c | c <- s]
-- ---------------------------------------------------------------------
-- Interpretaciones de una clausula --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- interpretacionesClausula :: Clausula -> [Interpretación]
-- tal que (interpretacionesClausula c) es el conjunto de
-- interpretaciones de c. Por ejemplo,
-- interpretacionesClausula [p, q, no p] ==> [[p,q],[p],[q],[]]
-- interpretacionesClausula [] ==> [[]]
-- ---------------------------------------------------------------------
interpretacionesClausula :: Clausula -> [Interpretación]
interpretacionesClausula c =
subconjuntos (simbolosProposicionalesClausula c)
-- ---------------------------------------------------------------------
-- Interpretaciones de un conjunto de clausulas --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- interpretacionesConjuntoClausula :: [Clausula] -> [Interpretación]
-- tal que (interpretacionesConjuntoClausula s) es el conjunto de
-- interpretaciones de s. Por ejemplo,
-- interpretacionesConjuntoClausula [[p, no q],[no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- interpretacionesConjuntoClausula []
-- ==> [[]]
-- ---------------------------------------------------------------------
interpretacionesConjuntoClausula :: [Clausula] -> [Interpretación]
interpretacionesConjuntoClausula c =
subconjuntos (simbolosProposicionalesConjuntoClausula c)
-- ---------------------------------------------------------------------
-- Modelos de clausulas --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- esModeloLiteral :: Interpretación -> Literal -> Bool
-- tal que (esModeloLiteral i l) se verifica si i es modelo de l. Por
-- ejemplo,
-- esModeloLiteral [p,r] p ==> True
-- esModeloLiteral [p,r] q ==> False
-- esModeloLiteral [p,r] (no p) ==> False
-- esModeloLiteral [p,r] (no q) ==> True
-- ---------------------------------------------------------------------
esModeloLiteral :: Interpretación -> Literal -> Bool
esModeloLiteral i (Atom s) = elem (Atom s) i
esModeloLiteral i (Neg (Atom s)) = notElem (Atom s) i
-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- esModeloClausula :: Interpretación -> Clausula -> Bool
-- tal que (esModeloClausula i c) se verifica si i es modelo de c . Por
-- ejemplo,
-- esModeloClausula [p,r] [p, q] ==> True
-- esModeloClausula [r] [p, no q] ==> True
-- esModeloClausula [q,r] [p, no q] ==> False
-- esModeloClausula [q,r] [] ==> False
-- ---------------------------------------------------------------------
esModeloClausula :: Interpretación -> Clausula -> Bool
esModeloClausula i c =
or [esModeloLiteral i l | l <- c]
-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- modelosClausula :: Clausula -> [Interpretación]
-- tal que (modelosClausula c) es la lista de los modelos de c. Por
-- ejemplo,
-- modelosClausula [no p, q] ==> [[p,q],[q],[]]
-- modelosClausula [no p, p] ==> [[p],[]]
-- modelosClausula [] ==> []
-- ---------------------------------------------------------------------
modelosClausula :: Clausula -> [Interpretación]
modelosClausula c =
[i | i <- interpretacionesClausula c,
esModeloClausula i c]
-- ---------------------------------------------------------------------
-- Modelos de conjuntos de clausulas --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- esModeloConjuntoClausulas :: Interpretación -> [Clausula] -> Bool
-- tal que (esModeloConjuntoClausulas i c) se verifica si i es modelo de
-- c. Por ejemplo,
-- esModeloConjuntoClausulas [p,r] [[p, no q], [r]] ==> True
-- esModeloConjuntoClausulas [p] [[p, no q], [r]] ==> False
-- esModeloConjuntoClausulas [p] [] ==> True
-- ---------------------------------------------------------------------
esModeloConjuntoClausulas :: Interpretación -> [Clausula] -> Bool
esModeloConjuntoClausulas i s =
and [esModeloClausula i c | c <- s]
-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- modelosConjuntoClausulas :: [Clausula] -> [Interpretación]
-- tal que (modelosConjuntoClausulas s) es la lista de los modelos de
-- s. Por ejemplo,
-- modelosConjuntoClausulas [[no p, q], [no q, p]]
-- ==> [[p,q],[]]
-- modelosConjuntoClausulas [[no p, q], [p], [no q]]
-- ==> []
-- modelosConjuntoClausulas [[p, no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- ---------------------------------------------------------------------
modelosConjuntoClausulas :: [Clausula] -> [Interpretación]
modelosConjuntoClausulas s =
[i | i <- interpretacionesConjuntoClausula s,
esModeloConjuntoClausulas i s]
-- ---------------------------------------------------------------------
-- Clausulas válidas, satisfacibles e insatisfacibles --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
-- esClausulaValida :: Clausula -> Bool
-- tal que (esClausulaValida c) se verifica si la clausula c es
-- válida. Por ejemplo,
-- esClausulaValida [p, q, no p] ==> True
-- esClausulaValida [p, q, no r] ==> False
-- esClausulaValida [] ==> False
-- ---------------------------------------------------------------------
esClausulaValida :: Clausula -> Bool
esClausulaValida c =
[l | l <- c, elem (complementario l) c] /= []
esClausulaValida1 :: Clausula -> Bool
esClausulaValida1 c =
or [elem (complementario l) c | l <- c]
-- Definición alternativa:
esClausulaValida2 :: Clausula -> Bool
esClausulaValida2 c =
and [esModeloClausula i c | i <- interpretacionesClausula c]
-- ---------------------------------------------------------------------
-- Ejercicio 16: Definir la función
-- esClausulaInsatisfacible :: Clausula -> Bool
-- tal que (esClausulaInsatisfacible c) se verifica si la clausula c es
-- insatisfacible. Por ejemplo,
-- esClausulaInsatisfacible [p, q, no p] ==> False
-- esClausulaInsatisfacible [p, q, no r] ==> False
-- esClausulaInsatisfacible [] ==> True
-- ---------------------------------------------------------------------
esClausulaInsatisfacible :: Clausula -> Bool
esClausulaInsatisfacible c =
null c
-- Definición alternativa:
esClausulaInsatisfacible1 :: Clausula -> Bool
esClausulaInsatisfacible1 c =
and [not (esModeloClausula i c) | i <- interpretacionesClausula c]
-- ---------------------------------------------------------------------
-- Ejercicio 17: Definir la función
-- esClausulaSatisfacible :: Clausula -> Bool
-- tal que (esClausulaSatisfacible c) se verifica si la clausula c es
-- satisfacible. Por ejemplo,
-- esClausulaSatisfacible [p, q, no p] ==> True
-- esClausulaSatisfacible [p, q, no r] ==> True
-- esClausulaSatisfacible [] ==> False
-- ---------------------------------------------------------------------
esClausulaSatisfacible :: Clausula -> Bool
esClausulaSatisfacible c =
not (null c)
-- Definición alternativa:
esClausulaSatisfacible1 :: Clausula -> Bool
esClausulaSatisfacible1 c =
or [esModeloClausula i c | i <- interpretacionesClausula c]
-- ---------------------------------------------------------------------
-- Conjuntos válidos, consistentes e inconsistentes de clausulas --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 18: Definir la función
-- esConjuntoValidoDeClausulas :: [Clausula] -> Bool
-- tal que (esConjuntoValidoDeClausulas s) se verifica si el conjunto de
-- clausulas s es válido. Por ejemplo,
-- esConjuntoValidoDeClausulas [[no p, q], [no q, p]] ==> False
-- esConjuntoValidoDeClausulas [[no p, p], [no q, q]] ==> True
-- esConjuntoValidoDeClausulas [] ==> True
-- ---------------------------------------------------------------------
esConjuntoValidoDeClausulas :: [Clausula] -> Bool
esConjuntoValidoDeClausulas s =
and [esClausulaValida c | c <- s]
-- Definición alternativa:
esConjuntoValidoDeClausulas1 :: [Clausula] -> Bool
esConjuntoValidoDeClausulas1 s =
modelosConjuntoClausulas s == interpretacionesConjuntoClausula s
-- ---------------------------------------------------------------------
-- Ejercicio 19: Definir la función
-- esConjuntoConsistenteDeClausulas :: [Clausula] -> Bool
-- tal que (esConjuntoConsistenteDeClausulas s) se verifica si el
-- conjunto de clausulas s es consistente. Por ejemplo,
-- esConjuntoConsistenteDeClausulas [[no p, q], [no q, p]] ==> True
-- esConjuntoConsistenteDeClausulas [[no p, p], [no q, q]] ==> True
-- esConjuntoConsistenteDeClausulas [] ==> True
-- ---------------------------------------------------------------------
esConjuntoConsistenteDeClausulas :: [Clausula] -> Bool
esConjuntoConsistenteDeClausulas s =
not (null (modelosConjuntoClausulas s))
-- ---------------------------------------------------------------------
-- Ejercicio 20: Definir la función
-- esConjuntoInconsistenteDeClausulas :: [Clausula] -> Bool
-- tal que (esConjuntoInconsistenteDeClausulas s) se verifica si el
-- conjunto de clausulas s es consistente. Por ejemplo,
-- esConjuntoInconsistenteDeClausulas [[no p,q],[no q,p]] ==> False
-- esConjuntoInconsistenteDeClausulas [[no p],[p]] ==> True
-- ---------------------------------------------------------------------
esConjuntoInconsistenteDeClausulas :: [Clausula] -> Bool
esConjuntoInconsistenteDeClausulas s =
null (modelosConjuntoClausulas s)
-- ---------------------------------------------------------------------
-- Validez de fórmulas mediante clausulas --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 21: Definir la función
-- esValidaPorClausulas :: Prop -> Bool
-- tal que (esValidaPorClausulas f) se verifica si el conjunto de
-- clausulas de f es válido. Por ejemplo,
-- esValidaPorClausulas (p --> q) ==> False
-- esValidaPorClausulas (p --> p) ==> True
-- esValidaPorClausulas ((p --> q) \/ (q --> p)) ==> True
-- ---------------------------------------------------------------------
esValidaPorClausulas :: Prop -> Bool
esValidaPorClausulas f =
esConjuntoValidoDeClausulas (clausulas f)
-- ---------------------------------------------------------------------
-- Consecuencia mediante clausulas --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 22: Definir la función
-- esConsecuenciaEntreClausulas :: [Clausula] -> [Clausula] -> Bool
-- tal que (esConsecuenciaEntreClausulas s1 s2) se verifica si todos los
-- modelos de s1 son modelos de s2. Por ejemplo,
-- esConsecuenciaEntreClausulas [[no p,q],[no q,r]] [[no p,r]]
-- ==> True
-- esConsecuenciaEntreClausulas [[p]] [[p],[q]]
-- ==> False
-- ---------------------------------------------------------------------
esConsecuenciaEntreClausulas :: [Clausula] -> [Clausula] -> Bool
esConsecuenciaEntreClausulas s1 s2 =
null [i | i <- interpretacionesConjuntoClausula (s1++s2)
, esModeloConjuntoClausulas i s1
, not ((esModeloConjuntoClausulas i s2))]
-- ---------------------------------------------------------------------
-- Ejercicio 23: Definir la función
-- esConsecuenciaPorClausulas1 :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorClausulas s f) se verifica si las clausulas
-- de f son consecuencias de las de s. Por ejemplo,
-- esConsecuenciaPorClausulas [(p --> q), (q --> r)] (p --> r)
-- ==> True
-- esConsecuenciaPorClausulas [p] (p /\ q)
-- ==> False
-- ---------------------------------------------------------------------
esConsecuenciaPorClausulas :: [Prop] -> Prop -> Bool
esConsecuenciaPorClausulas s f =
esConsecuenciaEntreClausulas (clausulasConjunto s) (clausulas f)
-- Definición alternativa:
esConsecuenciaPorClausulas1 :: [Prop] -> Prop -> Bool
esConsecuenciaPorClausulas1 s f =
esConjuntoInconsistenteDeClausulas (clausulasConjunto ((Neg f):s))
