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”