En la clase de hoy del curso Lógica Informática se han resuelto los ejercios propuestos de la sintaxis y semántica proposicional.
Concretamente, desde el ejercicio 22 al 32 del capítulo 1 del libro de ejercicios. Quedan pendientes para la próxima clase desde el 33 al 37.
El objetivo fundamental de la clase de hoy del curso Lógica Informáticaha consistido en responder estas dos preguntas:
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.
Se ha visto 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.
Finalmente, se ha presentado cómo se puede utilizar dos sistemas en la resolución de los anteriores problemas: Gateway to Logic y Prover9/Mace4.
Una implementación en Haskell de la semántica de la lógica proposicional siguiendo el contenido de esta clase se encuentra en el primer capítulo del libro Lógica en Haskell.
Los ejercicios pendientes para la próxima clase son desde el 26 al 37 del capítulo 1 del libro de ejercicios.
Las transparencias de esta clase son las páginas 14-34 del tema 1
Read More “LI2012: Semántica de la lógica proposicional”
La clase de hoy del curso Lógica Informática ha tenido dos partes.
En la primera parte se ha presentado la lógica proposicional como sistema de representación del conocimiento. También se ha presentado el sistema APLI2 que sirve de tutor para el aprendizaje de la representación lógica del conocimiento y el Prover9 como complemento para la corrección de errores sintácticos y determinación de la corrección de los argumentos. En la presentación se han resuelto los primeros 2 ejercicios.
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.
Las tareas propuestas son:
Las transparencias de esta clase son las páginas 2-13 del tema 1
Read More “LI2012: La lógica proposicional como sistema de representación del conocimiento y su sintaxis”
En la primera parte de la clase de hoy Lógica Informática se ha comentado las relaciones entre la lógica y la programación. Se han mostrado un programa con una máquina de Turing, un programa en Prolog y un demostrador proposicional en Haskell.
En la segunda parte he comentando relaciones entre las lógicas e informática:
En la clase de hoy, se ha realizado la presentación del 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: