Diferencia entre revisiones de «Ejercicio 3»
De Lógica matemática y fundamentos (2012-13)
| Línea 5: | Línea 5: | ||
* 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. | * 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. | * 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. | * 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 == | == Selección del ejercicio == | ||
Revisión del 11:30 26 abr 2013
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:
- 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: