LI2011

En la clase de hoy del curso Lógica Informática se ha presentado un nuevo sistema deductivo: los tableros semánticos. En este nuevo sistema se reduce el número de reglas del de deducción natural y se automatiza su aplicación.

Además, se ha presentado el sistema Tree Proof Generator que busca automáticamente el tablero semántico correspondiente a la fórmula introducida.

Como tarea pendientes se propone la resolución de los ejercicios del tema 3 del libro de ejercicios.

Las transparencias de esta clase son las del tema 3
Read More “LI2011: Tableros semánticos proposicionales”

En la clase de hoy del curso Lógica Informática se ha completado el estudio de la deducción natural en lógica proposicional.

La reglas que se han visto en la clase son las de la negción, las del bicondicional y las reglas derivadas (modus tollens, introducción de la doble negación, reducción al absurdo y ley del tercio excluso).

Como tarea pendientes se propone la resolución del ejercicio 5 del tema 2 del libro de ejercicios.

Las transparencias de esta clase son las páginas 13-28 del tema 1
Read More “LI2011: Deducción natural en lógica proposicional (2)”

En la clase de hoy del curso Lógica Informática se ha empezado el estudio de la deducción natural en lógica proposicional.

La reglas que se han visto en la clase son las de la conjunción, de la doble negación, de eliminación del condicional, de modus tollens, de introducción del condicional y las de la disyunción.

También se ha presentado el sistema Pandora para editar demostraciones por deducción natural.

Como tarea pendientes se propone la resolución de los 36 primeros apartados del ejercicio 5 del tema 2 del libro de ejercicios.

Las transparencias de esta clase son las páginas 1-12 del tema 1
Read More “LI2011: Deducción natural en lógica proposicional (1)”

En la clase de hoy del curso Lógica Informática se ha completado el estudio de la semántica proposicional desde el punto de vista computacional; es decir, se ha ido definidendo los conceptos semánticos y comentando su posible implementación.

Los 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

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.

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 rompecabeza se ha explicado el uso del Gateway to Logic.

Se ha comentado las soluciones de los ejercicios 25, 32 y 33 del tema 1.

Como tarea pendientes se propone la resolución de los restantes ejercicios del tema 1 del libro de ejercicios.

Las transparencias de esta clase son las páginas 26-34 del tema 1
Read More “LI2011: Semántica de la lógica proposicional (2)”

En la clase de hoy del curso Lógica Informática se ha comenzado el estudio de la semántica proposicional desde el punto de vista computacional; es decir, se ha ido definidendo los conceptos semánticos y comentando su posible implementación.

Los conceptos definidos son los valores de verdad, las funciones de verdad, las interprestaciones, 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 contigentes), 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.

Como tarea pendientes se propone la resolución de los ejercicios 11, 26, 32 y 33 del capítulo 1 del libro de ejercicios.

Las transparencias de esta clase son las páginas 14-25 del tema 1
Read More “LI2011: Semántica de la lógica proposicional (1)”