LI2014: Deducción natural proposicional (2)

En la la clase de hoy del curso de Lógica Informática se ha continuado el estudio de la deducción natural proposicional que se empezó en la clase anterior.

Las reglas que se han visto en la clase son las de la negació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 se ha propuesto la 3ª relación de ejercicios.

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

LI2014: Deducción natural proposicional (1)

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

Terminado el estudio semántico (cuyo problema fundamental es dado un conjunto de fórmulas S y una fórmula F, decidir si F es consecuencia de S (en notación, S |= F)), comenzamos 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, de la doble negación, de eliminación del condicional, de modus tollens, de introducción del condicional y las de la disyunción.

Finalmente, 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.

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

LI2014: Semántica de la lógica proposicional (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.

Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos.

También, se ha explicado cómo se puede usar en la resolución de los anteriores problemas el Gateway to Logic.

En la segunda parte de la clase se han comentado las soluciones de los ejercicios de la 1ª relación y se han propuesto los de la 2ª relación.

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

LI2014: Semántica de la lógica proposicional

El objetivo fundamental 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.

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