En la clase de hoy del curso Lógica Informática hemos comentado los tipos de ejercicios de los temas de lógica proposicional:
Hemos comentado las soluciones de los ejercicios propuestos de los temas 4 (formas normales) y 6 (algoritmo DPLL).
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos continuado el estudio de las definiciones por recursión en Haskell. Concretamente, hemos visto ejemplos de recursión con guardas, recursión sobre varios argumentos y recursión múltiple.
Las transparencias usadas en la clase son las comprendidas entre las páginas 10 y 13 del tema 6:
Read More “I1M2012: Definiciones por recursión (2)”
En la primera parte de la clase de hoy del curso Lógica Informática
hemos estudiado el algoritmo DPLL (Davis, Putnam, Logemann y Loveland).
En la seguna parte, hemos visto cómo resolver lógicamente problemas representándolos en la lógica proposicional y usando Prover9/Mace4 para su solución.
Los problemas que se han visto son
Las transparencias utilizadas son las del tema 6
Read More “LI2012: Algoritmos SAT. Aplicaciones de la lógica proposicional”
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones a los ejercicios de la 6ª relación que amplía la codificación César vista en clase para incluir las mayúsculas.
Los ejercicios, y sus soluciones, se muestran a continuación
Read More “I1M2012: Ejercicios sobre el cifrado César”
En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado la solución con Haskell de siguiente problema
Calcular el menor número natural n, mayor que 1, tal que para cualquier número entero x se verifique que x y xⁿ terminan en el mismo dígito.
La especificación matemática del enunciado es
min {n∈ℕ | n>1 ∧ ∀x∈ℤ (U(xⁿ) = U(x))}
donde U(x) es el último dígito de x. La especificación se puede reducir a
min {n∈ℕ | n>1 ∧ ∀x∈{0,…,9} (U(xⁿ) = U(x))}
Su traducción a Haskell es
|
1 2 3 |
solP3 :: Integer solP3 = head [n | n <- [2..], and [ultimo (x^n) == ultimo x | x <- [0..9]]] |
donde (ultimo x) es el último dígito de x
|
1 2 |
ultimo :: Integer -> Integer ultimo x = x `rem` 10 |
La solución del problema se calcula con
|
1 2 |
ghci> solP3 5 |
Se puede generalizar solP3 a una función solP3′ que calcula todos los números naturales n, mayores que 1, tales que para cualquier número entero x se verifique que x y xⁿ terminan en el mismo dígito. Para ello, basta eliminar head en la definición de solP3
|
1 2 3 |
solP3' :: [Integer] solP3' = [n | n <- [2..], and [ultimo (x^n) == ultimo x | x <- [0..9]]] |
El cálculo de los 20 primeros es
|
1 2 |
ghci> take 20 solP3' [5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81] |
Se observa que forman una progresión aritmética de diferencia 4. Basándonos en esta observación se puede redefinir solP3′ como sigue
|
1 2 |
solP3'' :: [Integer] solP3'' = [5,9..] |
Se puede comprobar experimentalmente la conjetura definiendo la función comprobacion tal que (comprobacion n) se verifica si los n primeros elementos de solP3′ son los mismos que los de solP3”.
|
1 2 3 |
comprobacion :: Int -> Bool comprobacion n = take n solP3' == take n solP3'' |
La comprobación para los 1000 primeros elementos es
|
1 2 |
ghci> comprobacion 1000 True |
Queda pendiente la demostración de la conjetura.