DAO2011: Deducción natural proposicional con Isabelle/HOL
En la clase de hoy del curso de Demostración asistida por ordenador (DAO2011) se ha estudiado cómo escribir demostraciones mediante deducción natural en lógica proposicional usando Isabelle/HOL/Isar.
La teoría correspondiente a la clase es Tema_3.thy cuyo contenido se muestra a continuación
Read More “DAO2011: Deducción natural proposicional con Isabelle/HOL”