-- ResolucionProposicional.hs
-- Resolución proposicional.
-- ---------------------------------------------------------------------
module ResolucionProposicional where
import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List
-- ---------------------------------------------------------------------
-- Resolventes --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- resolvente :: Clausula -> Clausula -> Literal -> Clausula
-- tal que (resolvente c1 c2 l) es la resolvente de c1 y c2 respecto del
-- literal l. Por ejemplo,
-- resolvente [no p,q] [no q,r] q ==> [no p,r]
-- resolvente [no p,no q] [q,r] (no q) ==> [no p,r]
-- resolvente [no p,q] [no p,no q] q ==> [no p]
-- ---------------------------------------------------------------------
resolvente :: Clausula -> Clausula -> Literal -> Clausula
resolvente c1 c2 l =
union (delete l c1) (delete (complementario l) c2)
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- resolventes :: Clausula -> Clausula -> [Clausula]
-- tal que (resolventes c1 c2) es el conjunto de las resolventes de c1 y
-- c2. Por ejemplo,
-- resolventes [no p,q] [p,no q] ==> [[q,no q],[no p,p]]
-- resolventes [no p,q] [p,q] ==> [[q]]
-- ---------------------------------------------------------------------
resolventes :: Clausula -> Clausula -> [Clausula]
resolventes c1 c2 =
[resolvente c1 c2 l | l <- c1, (complementario l) `elem` c2]
-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]
-- tal que (resolventes c s) es el conjunto de las resolventes de c y
-- s. Por ejemplo,
-- resolventesClausulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]
-- ==> [[q],[q,r],[no p,s]]
-- ---------------------------------------------------------------------
resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]
resolventesClausulaConjunto c s =
unionGeneral [resolventes c c1 | c1 <- s]
-- ---------------------------------------------------------------------
-- Eliminación de tautologías --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esTautologia :: Clausula -> Bool
-- tal que (esTautologia c) se verifica si c es una tautología. Por
-- ejemplo,
-- esTautologia [p, q, no p] ==> True
-- esTautologia [p, q, no r] ==> False
-- esTautologia [] ==> False
-- ---------------------------------------------------------------------
esTautologia :: Clausula -> Bool
esTautologia c =
[f | f <- c, elem (complementario f) c] /= []
esTautologia2 :: Clausula -> Bool
esTautologia2 c =
or [elem (complementario f) c | f <- c]
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- eliminaTautologias :: [Clausula] -> [Clausula]
-- tal que (eliminaTautologias s) es el conjunto obtenido eliminando las
-- tautologías de s. Por ejemplo,
-- eliminaTautologias [[p, q], [p, q, no p]] ==> [[p,q]]
-- ---------------------------------------------------------------------
eliminaTautologias :: [Clausula] -> [Clausula]
eliminaTautologias s =
[c | c <- s, not (esTautologia c)]
-- ---------------------------------------------------------------------
-- Decisión de inconsistencia por resolución --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- esInconsistentePorResolucion :: [Clausula] -> Bool
-- tal que (esInconsistentePorResolucion s) se verifica si s es
-- inconsistente mediante resolución. Por ejemplo,
-- esInconsistentePorResolucion [[p],[no p,q],[no q]]
-- ==> True
-- esInconsistentePorResolucion [[p],[no p,q]]
-- ==> False
-- esInconsistentePorResolucion [[p,q],[no p,q],[p,no q],[no p,no q]]
-- ==> True
-- esInconsistentePorResolucion [[p,q],[p,r],[no q,no r],[no p]]
-- ==> True
-- ---------------------------------------------------------------------
esInconsistentePorResolucion :: [Clausula] -> Bool
esInconsistentePorResolucion s =
esInconsistentePorResolucion' s []
esInconsistentePorResolucion' :: [Clausula] -> [Clausula] -> Bool
esInconsistentePorResolucion' soporte usables
| null soporte = False
| elem [] soporte = True
| otherwise =
esInconsistentePorResolucion' soporte' usables'
where actual = head soporte
usables' = union [actual] usables
soporte' = union (tail soporte)
[c
| c <- resolventesClausulaConjunto
actual
usables'
, not (esTautologia c)
, notElem c soporte
, notElem c usables']
-- ---------------------------------------------------------------------
-- Validez mediante resolución --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- esValidaPorResolucion :: Prop -> Bool
-- tal que (esValidaPorResolucion f) se verifica si f es válida por
-- resolución. Por ejemplo,
-- esValidaPorResolucion (p --> p) ==> True
-- esValidaPorResolucion ((p --> q) \/ (q --> p)) ==> True
-- esValidaPorResolucion (p --> q) ==> False
-- ---------------------------------------------------------------------
esValidaPorResolucion :: Prop -> Bool
esValidaPorResolucion f =
esInconsistentePorResolucion
(eliminaTautologias (clausulas (Neg f)))
-- ---------------------------------------------------------------------
-- Consecuencia mediante resolución --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorResolucion s f) se verifica si f es
-- consecuencia de s mediante el método de resolución. Por ejemplo,
-- esConsecuenciaPorResolucion [p --> q, q --> r] (p --> r)
-- ==> True
-- esConsecuenciaPorResolucion [p --> q, q --> r] (p <--> r)
-- ==> False
-- ---------------------------------------------------------------------
esConsecuenciaPorResolucion :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolucion s f =
esInconsistentePorResolucion
(eliminaTautologias (clausulasConjunto ((Neg f):s)))
