LMF2017: Sintaxis y semántica de la lógica proposicional

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se ha explicado la sintaxis de la lógica proposicional insistiendo en el carácter inductivo del tipo de datos de las fórmulas proposicionales, del procedimiento de definiciones por recursión sobre las fórmulas y de demostración de propiedades por inducción sobre las fórmulas.

Finalmente, se ha iniciado el estudio de la semántica de la lógica proposicional definiendo los booleanos, las interpretaciones, las funciones de verdad de las conectivas y mostrando cómo a partir de dichos conceptos se puede calcular el valor de verdad de una fórmula respecto de una interpretación.

A partir de lo anterior se han estudiado los modelos de fórmulas, la clasificación semántica de fórmulas (satisfacibles, insatisfacibles, tautologías, contradictorias y contingentes), los problemas SAT y TAUT. Finalmente, se han visto dos algoritmos para la solución de los problemas SAT y TAUT: tablas de verdad y método de Quine.

Otros conceptos definidos son equivalencia de fórmulas, modelos de conjuntos de fórmulas, conjuntos consistentes e inconsistentes y consecuencia lógica.

Finalmente, se ha hecho un ejemplo de formalización usando APLI2

Las transparencias de esta clase son las páginas 1-30 del tema 1.

I1M2017: Programación con Haskell en la Red usando Repl.it

PorJosé A. Alonso

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha explicado cómo programar con Haskell sólo de una conexión a la Red (ya sea en un ordenador que no tiene instalado Haskell, una tableta o un teléfono).

Para ello basta usar el sistema Repl.it que proporciona una sesión en la Red con Haskell (en concreto, la versión 8.0.1 de GHCi).

Como ejemplo se realizó la sesión grabada en el vídeo Haskell con Repl.it.

I1M2017: Resolución de problemas y el método de Polya

PorJosé A. Alonso

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha explicado el método de Polya de resolución de problemas.

La explicación se ha basado en la resolución del problema de cálculo eficiente del conjunto de divisores (que es la primera parte del problema propuesto ayer en Exercitium.

En primer lugar se consideró la solución elemental

Se comprueba que con dicha definición se resuelve los tres primeros ejemplos del enunciado del problema, pero no se resuelve el cuarto ejemplo. Por ello se plantea cómo mejorar la solución. Analizando el problema se ve que la clave está en considerar la factorización prima (que se calcula eficientemente con la función primeFactors de la librería Data.Numbers.Primes.

Trabajando con con ejemplo concreto (el cálculo de los divisores de 24) se observa las transformaciones que hay que hacer a la lista de los divisores primos de 24 para calcularlo.

Además, para una de esas transformaciones vemos que se puede usar otros de los problemas resueltos anteriormente en Exercitium: Producto cartesiano de una familia de conjuntos.

Una vez se tiene un plan para resolver el problema, se confirma haciendo los cálculos en una sesión de GHCi.

Ya sólo queda escribir la definición y comprobar que ha aumentado la eficiencia respecto de la primera solución y es capaz de calcular el cuarto ejemplo del enunciado del problema.

A continuación se comentó el método de Pólya para resolver problemas y se recomendó la lectura del libro de Polya Cómo plantear y resolver problemas.