Lógica matemática y fundamentos (2012-13) Lógica matemática y fundamentos (2012-13)

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: Alejandro Alfaro Martínez
• Ejercicio 2: Francisco Vilches Chacón
• Ejercicio 3: Salvador Joaquín Franco Peña
• Ejercicio 4: M Inmaculada Arjona Arjona
• Ejercicio 5: Pedro Ros Reina
• Ejercicio 6: Carmen Martinez Navarro
• Ejercicio 7: Ana Rocío del Valle
• Ejercicio 8:
• Ejercicio 9: Francisco Nieto Rueda
• Ejercicio 10: Gonzalo José Muñoz González-Meneses
• Ejercicio 11: José Antonio Jaime Sabín
• Ejercicio 12: Erlinda Menéndez Pérez
• Ejercicio 13: Concepción García Vidal
• Ejercicio 14:
• Ejercicio 15: Elena Villalba Calderón
• Ejercicio 16: Miguel Ángel Terrón Morgado
• Ejercicio 17: Jesús Horno Cobo
• Ejercicio 18: Lourdes Díaz Mena
• Ejercicio 19: Mª de los Remedios Sillero Denamiel
• Ejercicio 20: Antonio Jesús Molero del Río
• Ejercicio 21: Irene Araujo Guijo
• Ejercicio 22: FºJavier Sanz Gil
• Ejercicio 23:
• Ejercicio 24:
• Ejercicio 25: Pedro José Perea Rojo
• Ejercicio 26: José María Contreras Beltrán
• Ejercicio 27: Isabel Duarte Tosso
• Ejercicio 28: Miriam Núñez-Romero Olmo