LMF2013: Resolución proposicional en Haskell
En la primera parte de la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) se ha comentado las soluciones de los ejercicios sobre la implementación en Haskell de la resolución proposicional.
Las soluciones de los ejercicios se muestran a continuación. En los ejercicios se usa los módulos
desaroolado en clases anteriores.
La implementación de resolución comentada es
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 |
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 :: Cláusula -> 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] /= [] -- --------------------------------------------------------------------- -- Ejercicio 2: Definir la función -- eliminaTautologias :: [Cláusula] -> [Cláusula] -- 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 -- esValidaPorResolución :: Prop -> Bool -- tal que (esValidaPorResolución f) se verifica si f es válida por -- resolución. Por ejemplo, -- esValidaPorResolución (p --> p) ==> True -- esValidaPorResolución ((p --> q) \/ (q --> p)) ==> True -- esValidaPorResolución (p --> q) ==> False -- --------------------------------------------------------------------- esValidaPorResolución :: Prop -> Bool esValidaPorResolución 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))) |