LI2011-12: Deducción natural en lógica de primer orden
La clase de hoy del curso Lógica Informática ha tenido dos partes.
En la primera parte, se ha comentado formalizaciones de argumentos en la lógica de primer orden usando APLI2. En concreto, los ejercicios 2, 3, 7, 8, 9 y 12. También hemos visto una forma de facilitar la corrección de los errores sintácticos: escribir la fórmula en Prover9 y preguntarle si está bien escrita.
En la segunda parte, se ha presentado la ampliación del cálculo de deducción natural proposional para tratar los cuantificadores y las igualdades.
También se ha presentado el sistema Pandora para editar demostraciones por deducción natural.
Las transparencias de esta clase son las del tema 7 que se muestran a continuación
Como tarea se propone la resolución de los ejercicios del tema 7 del libro de ejercicios.