LI2015

En la primera parte de la clase de hoy del curso de Lógica Informática se ha continuado el estudio de la lógica proposicional.

Las reglas que se han visto en la clase de hoy son las de eliminación del condicional, de modus tollens, de introducción del condicional y las de la disyunción.

También se ha mostrado cómo editar demostraciones usando el sistema Pandora. Los ejemplos vistos en clase se encuentran en los vídeos del ejemplo 1 y ejemplo 2.

En la segunda parte de la clase se han comentado la solución del ejercicio 30.2 del capítulo 1 del libro de ejercicios y cómo ver la corrección del argumento con distintos sistemas de cálculo de tablas de verdad:

• Logica (Tools for Logic): Boole,
• BoolTool y
• Truth tables.

Se propusieron para la próxima clase los 37 primeros apartados del ejercicio 2.5 del libro de ejercicios.

Las transparencias de esta clase son las páginas 1-12 del tema 2

En la primera parte de la clase de hoy del curso de Lógica Informática se ha demostrado la equivalencia de los siguientes problemas

1. decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
2. decidir si una fórmula es una tautología,
3. decidir si una fórmula es insatisfacible y
4. decidir si un conjunto de fórmulas es inconsistente.

A continuación, se ha comentado distintos tipos de problemas que se pueden plantear sobre la sintaxis y semántica de la lógica proposicional.

Finalmente, se ha comenzado el estudio de los cálculos deductivos (cuyo problema fundamental es dado un conjunto de fórmulas S y una fórmula F, decidir si F es deducible de S (en notación, S ⊢ F)). Además, se requiere que los cálculos sean adecuados y completos (es decir; que S ⊧ F si, y sólo si, S ⊢ F).

El primer cálculo deductivo que estudiamos es el de deducción natural. Las reglas que se han visto en la clase de hoy son las de la conjunción y de la doble negación.

En la segunda parte de la clase se han comentado las soluciones de los ejercicios 26.1, 27.1, 28, 29.2, 30.1 del capítulo 1 del libro de ejercicios. En la solución del último, se ha explicado cómo comprobar las formalizaciones usando APLI2.

Se propusieron para la próxima clase los ejercicios 32 a 37 del capítulo 1 del libro de ejercicios.

Las transparencias de esta clase son las páginas 1-5 del tema 2

El objetivo fundamental de primera parte de la clase de hoy del curso Lógica Informática ha consistido en responder estas dos preguntas:

• ¿cómo se puede construir un programa para que dada una fórmula decida si es verdadera?
• ¿cómo se puede construir un programa para que dada un conjunto de fórmulas S una fórmula F decida si es consecuencia de S?

Para responder a la primera pregunta, desarrollamos la semántica de la lógica proposicional. En primer lugar, el valor de verdad de una fórmula en una interpretación se define por recursión. A partir del valor de verdad podemos, dada una fórmula F, dividir las interpretaciones entre las que son modelo de F y las que no lo son. Además, las fórmulas pueden clasificarse en satisfacibles (las que tienen modelos) e insatisfacibles (en caso contrario). Las fórmulas satisfacibles se pueden clasificar en tautologías (para las que todas las interpretaciones son modelo) y contingentes (en caso contrario).

Hemos continuado planteando los problemas SAT y TAUT y presentando dos algoritmos para su solución: tablas de verdad y método de Quine.

Además, se han definidos los conceptos de equivalencia de fórmulas, modelos de conjuntos de fórmulas, conjuntos consistentes e inconsistentes y la relación de consecuencia lógica.

En la segunda parte de la clase se han comentado las soluciones de los ejercicios 22, 23, 24.1 y 25 del capítulo 1 del libro de ejercicios. Se propusieron para la próxima clase los ejercicios 26 a 31.

Las transparencias de esta clase son las páginas 14-34 del tema 1

La clase de hoy del curso Lógica Informática ha tenido dos partes.

En la primera parte se ha presentado un panorama de la lógica y sus aplicaciones a la informática.

En la segunda parte 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 como respuesta a la siguiente pregunta

• ¿cómo se puede construir un programa para que dada una fórmula decida si es verdadera?

Para responder la primera pregunta, empezamos definiendo, por recursión, el valor de verdad de una fórmula en una interpretación. A partir del valor de verdad podemos, dada una fórmula F, dividir las interpretaciones entre las que son modelo de F y las que no lo son. Además, las fórmulas pueden clasificarse en satisfacibles (las que tienen modelos) e insatisfacibles (en caso contrario). Las fórmulas satisfacibles se pueden clasificar en tautologías (para las que todas las interpretaciones son modelo) y contingentes (en caso contrario).

Hemos continuado planteando los problemas SAT y TAUT y presentando dos algoritmos para su solución: tablas de verdad y método de Quine.

Como tarea se ha propuesto resolver de los ejercicios 22 a 27 del capítulo 1 del libro de ejercicios (páginas 11 y 12).

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

En la clase de hoy, se ha presentado el curso Lógica Informática 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:

• la página de la asignatura,
• las transparencias de los temas.
• el libro con los apuntes de los temas
• el libro con los enunciados de los ejercicios y
• el libro de exámenes resueltos de cursos anteriores.