LI2013: Sintaxis de la lógica proposicional
La clase de hoy del curso Lógica Informática ha tenido tres partes.
En la primera parte se ha comentado las soluciones de la 1ª relación de ejercicios de representación del conocimiento en lógica proposicional usando Isabelle/HOL.
En la segunda parte se ha presentado un panorama de la lógica y sus aplicaciones a la informática. Como ejemplo de aplicación se ha mostrado cómo se puede generar automáticamente programas usando MagicHaskeller.
En la tercera 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:
- resolver los ejercicios de la 2ª relación de representación del conocimiento proposicional en Isabelle/HOL y
- resolver los ejercicios 22 a 24 del tema 2 (páginas 11 y 12 del libro de ejercicios).
Las transparencias de esta clase son las páginas 2-13 del tema 1