En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la deducción natural en la lógica proposicional.
También se ha presentado cómo escribir demostraciones por deducción natural en Pandora del que se mostró un videotutorial.
Las transparencias de estas clases son las del tema 2
En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la sintaxis y la semántica de la lógica proposicional.
Se ha presentado la sintaxis de la lógica proposicional. Concretamente,
En la semántica, los conceptos definidos son los valores de verdad, las funciones de verdad, las interpretaciones, el valor de verdad de las fórmulas respectos de las interpretaciones, 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.
Se ha demostrado la equivalencia de los siguientes problemas
Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos. En la solución del rompecabezas se ha explicado el uso del Gateway to Logic.
Las transparencias de estas clases son las del tema 1
Read More “LMF2014: Sintaxis y semántica de la lógica proposicional”
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo definir el tipo de las fórmulas proposicionales y, trabajando con dicho tipo, construir un programa para determinar si una fórmula es una tautología.
El código correspondiente es
Read More “I1M2013: Un programa en Haskell para decidir tautologías”
En la clase de hoy, se ha realizado la presentación del curso Lógica matemática y fundamentos siguiendo el plan de la asignatura.
Se ha comentado el contenido de la asignatura, el sistema de evaluación y los materiales de la asignatura en la Red:
En la clase de hoy del curso de Razonamiento automático se ha continuado el estudio de la deducción natural en lógica proposicional con Isabelle/HOL. La presentación se basa en los ejemplos de tema 2 del curso LI (Lógica informática), que a su vez se basa en el libro de de Huth y Ryan Logic in Computer Science. La página al lado de cada ejemplo indica la página de las transparencias de LI donde se encuentra la demostración.
Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de la transparencia, las siguientes van eliminando detalles de la prueba hasta la última que es automática.
A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2013: Deducción natural en lógica proposicional con Isabelle/HOL (2)”