En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha realizado el 2º examen de la evaluación continua.
A continuación se muestra el examen junto con su solución:
Read More “I1M2012: 2º examen de la evaluación continua”
En la sesión de hoy del seminario Demostración asistida por ordenador (DAO2012) se ha presentado cómo se puede hacer con Isabelle/HOL demostraciones por deducción natural en la lógica proposicional.
La presentencaión se realiza a través de los ejemplos del tema de deducción natural proposicional del libro de Huth y Ryan Logic in Computer Science y, más concretamente, a la forma como se explica en la asignatura de Lógica informática (LI).
La página al lado de cada ejemplo indica la página de las transparencias
de LI donde se encuentra la demostración.
La teoría correspondiente a la clase es DNLP.thy cuyo contenido se muestra a continuación
Read More “DAO2012: Deducción natural proposicional con Isabelle/HOL”
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado la solución con Haskell de un problema propuesto para la Olimpiada Internacional de Matemáticas de 1987 cuyo enunciado es
”Calcular el menor número natural n tal que n! termina exactamente en 1987 ceros.”
Resolverlo con Haskell.
Para resolverlo, empezamos definiendo la función cerosDelFactorial tal que (cerosDelFactorial n) es el número de ceros en que termina el factorial de n. Por ejemplo,
|
1 2 |
cerosDelFactorial1 24 == 4 cerosDelFactorial1 25 == 6 |
Presentamos dos definiciones la primera es
|
1 2 |
cerosDelFactorial1 :: Integer -> Integer cerosDelFactorial1 n = ceros (factorial n) |
donde (ceros n) es el número de ceros en los que termina el número n. Por ejemplo,
|
1 |
ceros 320000 == 4 |
|
1 2 |
ceros n | rem n 10 /= 0 = 0 | otherwise = 1 + ceros (div n 10) |
y (factorial n) es el factorial n. Por ejemplo,
|
1 |
factorial 3 == 6 |
|
1 |
factorial n = product [1..n] |
La segunda es
|
1 2 3 4 |
cerosDelFactorial2 :: Integer -> Integer cerosDelFactorial2 n | n < 5 = 0 | otherwise = m + cerosDelFactorial2 m where m = n `div` 5 |
Se puede comprobar la equivalencia de las dos definiciones
|
1 2 |
ghci> and [cerosDelFactorial1 n == cerosDelFactorial2 n | n <- [1..100]] True |
y que la segunda es más eficiente
|
1 2 3 4 5 6 |
ghci> cerosDelFactorial1 (10^4) 2499 (0.64 secs, 131287116 bytes) ghci> cerosDelFactorial2 (10^4) 2499 (0.01 secs, 725088 bytes) |
En lo que sigue, usaremos la segunda definición
|
1 2 |
cerosDelFactorial :: Integer -> Integer cerosDelFactorial = cerosDelFactorial1 |
A continuación definimos la función menorFactorial tal que (menorFactorial m) es el menor número cuyo factorial termina en m ceros exactamente. Por ejemplo,
|
1 2 3 |
menorFactorial 1 == 5 menorFactorial 4 == 20 menorFactorial 6 == 25 |
|
1 2 |
menorFactorial :: Integer -> Integer menorFactorial k = head [n | n <- [1..], cerosDelFactorial n == k] |
Finalmente definimos la solución del problema; es decir, el menor número natural n tal que n! termina exactamente en 1987 ceros.
|
1 2 |
solucion :: Integer solucion = menorFactorial 1987 |
El cálculo de la solución es
|
1 2 |
ghci> solucion 7960 |
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los problemas 8 (números bonitos y números feos) y 9 (ceros finales del factorial).
En la segunda parte hemos comentado las soluciones de los ejercicios 4 y 6 de la 12ª relación de funciones sobre cadenas.
Los ejercicios, y sus soluciones, se muestran a continuación:
Read More “I1M2012: Problemas 8 y 9 y ejercicios sobre cadenas”
En la clase de hoy del curso Lógica Informática se estudiado cómo se puede puede reducir 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.