Ejercicio 2

Enunciado

El segundo ejercicio evaluable consiste en la realización de una demostración por deducción natural en la Lógica de primer orden, con Isabelle/HOl. Para ello,

• Cada alumno elegirá uno de los ejercicios propuestos en T2).
• Una vez elegido, lo anotará en la lista que se muestra a continuación, no pudiendo un mismo ejercicio ser elegido por dos alumnos.
• El ejercicio resuelto se enviará en un fichero usuario_2.thy.
• En la valoración del ejercicio se tendrá en cuenta tanto el nivel de dificultad como la calidad de la demostración.

Selección del ejercicio

• Ejercicio 1:
• Ejercicio 2:
• Ejercicio 3:
• Ejercicio 4:
• Ejercicio 5:
• Ejercicio 6:
• Ejercicio 7:
• Ejercicio 8:
• Ejercicio 9:
• Ejercicio 10:
• Ejercicio 11:
• Ejercicio 12:
• Ejercicio 13:
• Ejercicio 14:
• Ejercicio 15:
• Ejercicio 16:
• Ejercicio 17:
• Ejercicio 18:
• Ejercicio 19:
• Ejercicio 20:
• Ejercicio 21:
• Ejercicio 22:
• Ejercicio 23:
• Ejercicio 24:
• Ejercicio 25:
• Ejercicio 26:
• Ejercicio 27:
• Ejercicio 28:
• Ejercicio 29:
• Ejercicio 30:
• Ejercicio 31:
• Ejercicio 32:
• Ejercicio 33: