Lecturas del Grupo de Lógica Computacional (de julio de 2013 a marzo de 2014)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional o en mi página de twitter desde la anterior recopilación.

La recopilación está ordenada por la fecha de su publicación en la lista o en twitter. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

Read More “Lecturas del Grupo de Lógica Computacional (de julio de 2013 a marzo de 2014)”

LMF2014: Ejercicios de deducción en lógica de primer orden con Isabelle/HOL

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se ha explicado cómo demostrar mediante deducción natural teoremas de primer orden con Isabelle/HOL. En concreto, se han visto los ejercicios 1, 5, 9, 10, 20 y 27 de la relación 6.

Los ejercicios y sus soluciones se muestran a continuación:
Read More “LMF2014: Ejercicios de deducción en lógica de primer orden con Isabelle/HOL”

LMF2014: Deducción natural en lógica de primer orden

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la primera parte de la deducción natural en la lógica de primer orden.

Las transparencias de estas clases son las páginas 1 a 13 del tema 8.

A la vez que se presentaba las reglas, se ha comentado su formalización en Isabelle/HOL. La teoría correspondiente es
Read More “LMF2014: Deducción natural en lógica de primer orden”