Ejercicio 3

Enunciado

El tercer ejercicio evaluable consiste en la realización de un ejercicio de argumentación en lógica de primer orden, haciendo la demostración por deducción natural con Isabelle/HOL y por tableros semánticos. Para ello,

• Cada alumno elegirá uno de los ejercicios propuestos en E3.
• Una vez elegido, lo anotará en la lista que se muestra a continuación, no pudiendo un mismo ejercicio ser elegido por más de un alumno.
• Se enviará a mjoseh@us.es antes del viernes 10 de mayo de 2013, dos ficheros: uno usuario_3a.thy con la prueba por deducción natural y otro con la prueba por tableros.
• Los lemas que se usen en una demostración tendrán que ser probados de forma no automática.
• 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: Francisco Vilches Chacón
• Ejercicio 3:
• Ejercicio 4: M Inmaculada Arjona Arjona
• Ejercicio 5:
• Ejercicio 6:
• Ejercicio 7:
• Ejercicio 8:
• Ejercicio 9:
• Ejercicio 10: Gonzalo José Muñoz González-Meneses
• Ejercicio 11: José Antonio Jaime Sabín
• Ejercicio 12:
• Ejercicio 13:
• Ejercicio 14: Carmen Martínez Navarro
• Ejercicio 15:
• Ejercicio 16:
• Ejercicio 17:
• Ejercicio 18:
• Ejercicio 19: Mª de los Remedios Sillero Denamiel
• Ejercicio 20: Antonio Jesús Molero del Río
• Ejercicio 21: Irene Araujo Guijo
• Ejercicio 22:
• Ejercicio 23:
• Ejercicio 24:
• Ejercicio 25:
• Ejercicio 26: José María Contreras Beltrán
• Ejercicio 27: Isabel Duarte Tosso
• Ejercicio 28: