En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha realizado el 5º examen de la evaluación continua.
A continuación se muestra el examen junto con su solución:
Read More “I1M2012: 5º examen de la evaluación continua”
Se ha publicado un trabajo de verificación formal con Coq titulado A certified reduction strategy for homological image processing.
Sus autores son María Poza, César Domínguez, Jónathan Heras y Julio Rubio (de la Universidad de la Rioja).
Su resumen es
The analysis of digital images using homological procedures is an outstanding topic in the area of Computational Algebraic Topology. In this paper, we describe a certified reduction strategy to deal with digital images, but preserving their homological properties. We stress both the advantages of our approach (mainly, the formalisation of the mathematics allowing us to verify the correctness of algorithms) and some limitations (related to the performance of the running systems inside proof assistants). The drawbacks are overcome using techniques that provide an integration of computation and deduction. Our driving application is a problem in bioinformatics, where the accuracy and reliability of computations are specially requested.
El código de las teoría Coq correspondientes al trabajo se encuentra aquí.
En la segunda parte de la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) hemos estudiado el algoritmo DPLL (Davis, Putnam, Logemann y Loveland).
Además, se ha comentado la propuesta del 4º ejercicio evaluable consistente en la implementación en Haskell del algoritmo de DPLL y de refinamientos de resolución.
Las transparencias utilizadas son las del tema 6
Read More “LMF2013: Algoritmo DPLL (Davis, Putnam, Logemann y Loveland)”
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))) |
En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado cómo puede puede reducirse la consistencia de conjuntos de cláusulas de primer orden a la consistencia de conjuntos de cláusulas proposicionales.
En primer lugar, se ha observado que la reducción es inmediata en el caso de fórmulas sin variables.
A continuación se han presentado procedimientos para construir los universos de Herbrand, las bases de Herbrand y las interpretaciones de Herbrand. Así como un procedimiento que transforma modelos de conjuntos de cláusulas en modelos de Herbrand. Por tanto, la consistencia de un conjunto de cláusulas se reduce a la búsqueda de modelos de Herbrand.
Finalmente, se ha explicado el teorema de Herbrand y su aplicación para decidir la consistencia de un conjunto de cláusulas buscando un subconjunto finito de su extensión de Herbrand que sea consistente (en el sentido proposicional).
Las transparencias de la clase son las del tema 11.