Isabelle/HOL

<

p>En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la segunda parte de la deducción natural en la lógica de primer orden. En concreto, la demostración de equivalencias lógicas y las reglas de la igualdad

<

p>Las transparencias de estas clases son las páginas 14 a 29 del tema 8.

<

p>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 (2)”

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”

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”

En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos se ha explicado cómo formalizar en lógica proposicional los argumentos de los ejercicios 3 y 9 de la relación 4 y cómo demostrar con Isabelle/HOL su corrección.

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