DAO2012: Deducción natural proposicional con Isabelle/HOL

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”

I1M2012: Ceros finales del factorial

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,

Presentamos dos definiciones la primera es

donde (ceros n) es el número de ceros en los que termina el número n. Por ejemplo,

y (factorial n) es el factorial n. Por ejemplo,

La segunda es

Se puede comprobar la equivalencia de las dos definiciones

y que la segunda es más eficiente

En lo que sigue, usaremos la segunda definición

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,

Finalmente definimos la solución del problema; es decir, el menor número natural n tal que n! termina exactamente en 1987 ceros.

El cálculo de la solución es

I1M2012: Problemas 8 y 9 y ejercicios sobre cadenas

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”

LI2012: Modelos de Herbrand

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.