Deducción natural en lógica de primer orden con Isabelle/Isar
En esta teoría se presenta la formalización en Isabelle/Isar de los ejemplos del tema de deducción natural en la lógica de primer orde siguiendo la presentación de Huth y Ryan en su libro Logic in Computer Science y, más concretamente, a la forma como se explica en la asignatura de Lógica informática y que puede verse en las transparencias del tema 7.
La páginas en los teorema indican la página de las anteriores transparencias donde se encuentra la demostración.
Read More “Deducción natural en lógica de primer orden con Isabelle/Isar”