Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

Relaciones de ejercicios propuestos

• Relación 1: Deducción natural proposicional en Isabelle/HOL. (Enunciado).
• Relación 2: Deducción natural en Lógica de primer orden en Isabelle/HOL. (Enunciado).
• Relación 3: Programación funcional en Isabelle/HOL. (Enunciado).
• Relación 4: Razonamiento sobre programas en Isabelle/HOL. (Enunciado).
• Relación 5: Cuantificadores sobre listas. (Enunciado).
• Relación 6: Recorridos sobre árboles. (Enunciado).
• Relación 7: Caso de estudio: Clausura reflexiva, simétrica y transitiva de una relación binaria. (Enunciado).
• Relación 8: Expresiones aritméticas: ejercicios.(Enunciado).
• Relación 9: Expresiones booleanas: ejercicios.(Enunciado).
• Relación 10: Semántica operacional de IMP: ejercicios.(Enunciado).
• Relación 11: Lógica de Hoare: ejemplos.(Enunciado).
• Relación 12: Lógica de Hoare: programas anotados.(Enunciado).