Ejercicios RA2013
De DAO (Demostración asistida por ordenador)
Revisión del 20:12 1 abr 2013 de Jalonso (discusión | contribuciones) (→Ejercicios de Demostración asistida por ordenador)
Ejercicios de Demostración asistida por ordenador
En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por los alumnos del curso y no deben tomarse como definitivas.
- Relación 1: Deducción natural en lógica proposicional con Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 2: Argumentación proposicional con Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 3: Eliminación de conectivas. (Enunciado y Solución colaborativa).
- Relación 4: Deducción natural en lógica de primer con Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 5: Argumentación en lógica de primer con Isabelle/HOL. (Enunciado y Solución colaborativa).
- Relación 6: Argumentación en lógica de primer orden e igualdad con Isabelle/HOL. (Enunciado y Solución colaborativa).