En la clase de hoy del curso de Razonamiento automático se han presentado las técnicas de demostración en Isabelle por inducción sobre tipos recursivos. En concreto se han estudiado los esquemas de inducción para las listas y para los árboles binarios.
Las transparencias usadas en clase son las páginas 31-34 del tema 3 (Distinción decasos e inducción). El código correspondiente se encuentra en Cap_3.thy.
La clase de hoy del curso de Razonamiento automático ha tenido dos partes. En la primera parte se ha comentado la historia del razonamiento automático y algunos de sus logros. En la segunda parte se ha continuado la introducción de técnicas de demostración en Isabelle estudiando la demostración por inducción sobre los números naturales.
Las transparencias y apuntes usados en clase son los siguientes:
La tarea pendiente para la próxima clase consiste en escribir, y publicar en el portafolio digital, las soluciones de los ejercicios de la relación 1 y de la relación 2. Los códigos se encuentran el la página de ejercicios.
En la clase de hoy del curso de Razonamiento automático se ha visto cómo se puede escribir en Isabelle/Isar demostraciones de la lógica de primer orden, el razonamiento ecuacional y las demostraciones por casos.
En la clase se ha presentado el tema 2 (desde la página 21 a la 26) y el tema 3 (desde la página 26 a la 28)
El código correspondiente se encuentra en Cap_2.thy y Cap_3.thy–
Las clases de esta semana del curso de Razonamiento automático se han sustituido por las conferencias de las Jornadas de Lógica, Computación e Inteligencia Artificial
En dichas Jornadas, he presentado las investigaciones en Lógica
computacional realizadas por el Grupo de Lógica Computacional de la Universidad de Sevilla.
El título de la presentación fue Lógica Computacional en Sevilla (30 años en una hora).
Read More “RA2010: Investigación en lógica computacional”
La clase de hoy del curso de Razonamiento automático ha consistido en la formalización en Isabelle/Isar de demostraciones por deducción natural en lógica proposicional. Para ello se han formalizado todas las demostraciones del tema de deducción natural proposicional del curso de Lógica informática
Las formalizaciones realizadas en clase se encuentran en el siguiente documento
Read More “RA2010: Ejercicios de razonamiento proposicional con Isabelle”