En la clase de hoy del curso de Demostración asistida por ordenador se han comentado las soluciones de los ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL/Isar.
A continuación se muestra la teoría correspondiente a las soluciones de los ejercicios
Read More “DAO2011: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL”
En la clase de hoy del curso de Demostración asistida por ordenador se se ha estudiado cómo escribir demostraciones mediante deducción natural en lógica de primer orden 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 en lógica de primer orden con Isabelle/HOL”
En la clase de hoy del curso de Demostración asistida por ordenador se han comentado las soluciones de los ejercicios de deducción natural proposicional con Isabelle/HOL/Isar.
A continuación se muestra la teoría correspondiente a los enunciados de los ejercicios
Read More “DAO2011: Ejercicios de 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”
En la clase de hoy del curso de Demostración asistida por ordenador se han comentado las soluciones propuestas por los alumnos a los ejercicios de demostración con Isabelle de propiedades de programas funcionales.
La teoría correspondiente a la clase es Relacion_1.thy cuyo contenido se muestra a continuación
Read More “DAO2011: Ejercicios de razonamiento sobre programas con Isabelle”