Lógica matemática y fundamentos (2014-15) Lógica matemática y fundamentos (2014-15)

-- 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 :: Cláusula -> Cláusula -> Literal -> Cláusula
-- 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]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
resolvente c1 c2 l = nub (filter (/= l )(filter 
                        (/= (complementario l)) (c1 ++ c2)))

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
--    resolventes :: Cláusula -> Cláusula -> [Cláusula]
-- 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]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolventes :: Cláusula -> Cláusula -> [Cláusula]
resolventes c1 c2 = [resolvente c1 c2 l | l <- c1, 
                              elem (complementario l) c2 ]

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
--    resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
-- tal que (resolventes c s) es el conjunto de las resolventes de c y
-- s. Por ejemplo, 
--    resolventesCláusulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]
--    ==> [[q],[q,r],[no p,s]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
resolventesCláusulaConjunto c s = aux c s
                                 where aux x [] = []
                                       aux x (y:ys) = resolventes x y ++ 
                                                      aux x ys

-- ---------------------------------------------------------------------
-- Eliminación de tautologías                                         --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
--    esTautología :: Cláusula -> Bool
-- tal que (esTautología c) se verifica si c es una tautología. Por
-- ejemplo, 
--    esTautología [p, q, no p]  ==>  True
--    esTautología [p, q, no r]  ==>  False
--    esTautología []            ==>  False
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

esTautología :: Cláusula -> Bool
esTautología c = or [elem (complementario x) c | x <- c]

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
--    eliminaTautologías :: [Cláusula] -> [Cláusula]
-- tal que (eliminaTautologías s) es el conjunto obtenido eliminando las
-- tautologías de s. Por ejemplo,
--    eliminaTautologías [[p, q], [p, q, no p]]  ==>  [[p,q]]
-- ---------------------------------------------------------------------

-- Francisco Javier Carmona

eliminaTautologías :: [Cláusula] -> [Cláusula]
eliminaTautologías s = [ x | x <- s, not( esTautologia x)]

-- ---------------------------------------------------------------------
-- Decisión de inconsistencia por resolución                          --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
--    esInconsistentePorResolución :: [Cláusula] -> Bool
-- tal que (esInconsistentePorResolución s) se verifica si s es
-- inconsistente mediante resolución. Por ejemplo,
--    esInconsistentePorResolución [[p],[no p,q],[no q]]
--    ==> True
--    esInconsistentePorResolución [[p],[no p,q]]
--    ==> False
--    esInconsistentePorResolución [[p,q],[no p,q],[p,no q],[no p,no q]]
--    ==> True
--    esInconsistentePorResolución [[p,q],[p,r],[no q,no r],[no p]]
--    ==> True
-- ---------------------------------------------------------------------

-- Luis Palma, no hay acentos

esInconsistentePorResolución :: [Cláusula] -> Bool
esInconsistentePorResolución s = esConjuntoInconsistenteDeClausulas s

-- La solución anterior no es correcta ya que esta resuelta por clausula,
-- no por resolución, la propuesta en clase es:

esInconsistentePorResolucion1 :: [Clausula] -> Bool
esInconsistentePorResolucion1 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
--    esVálidaPorResolución :: Prop -> Bool
-- tal que (esVálidaPorResolución f) se verifica si f es válida por
-- resolución. Por ejemplo, 
--    esVálidaPorResolución (p --> p)                 ==>  True
--    esVálidaPorResolución ((p --> q) \/ (q --> p))  ==>  True
--    esVálidaPorResolución (p --> q)                 ==>  False
-- ---------------------------------------------------------------------

--Luis Palma

esVálidaPorResolución :: Prop -> Bool
esVálidaPorResolución f = esConjuntoValidoDeClausulas (clausulas f)

-- ---------------------------------------------------------------------
-- Consecuencia mediante resolución                                   --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
--    esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorResolución s f) se verifica si f es
-- consecuencia de s mediante el método de resolución. Por ejemplo,
--    esConsecuenciaPorResolución [p --> q, q --> r] (p --> r)  
--    ==> True
--    esConsecuenciaPorResolución [p --> q, q --> r] (p <--> r)
--    ==> False
-- ---------------------------------------------------------------------

-- Luis Palma

esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolución s f =  esInconsistentePorResolucion (clausulasConjunto ((Neg f):s))