[Práctico 1] Ejercicios 1.11 y 1.12

[Práctico 1] Ejercicios 1.11 y 1.12

de Juan Manuel Rivara De Leon -
Número de respuestas: 1

Tengo un par de consultas sobre el práctico 1.

En el ejercicio 11, la parte b) pide demostrar que las reglas son contradictorias, y el ejercicio c) pide probar que las reglas son contradictorias. No entiendo en este contexto la diferencia entre demostrar y probar. Y en lo que respecta a la prueba automática, ¿ésta tiene que probar de principio a fin la contradicción o hay que usar tauto en un paso intermedio (es decir, hacer al menos parte de la demostración manualmente)?

La otra pregunta es si en el ejercicio 12 se aplica la lógica clásica (con tercero excluído) o hay que hacer un diagnóstico puramente constructivo.

Saludos.

En respuesta a Juan Manuel Rivara De Leon

Re: [Práctico 1] Ejercicios 1.11 y 1.12

de Carlos Luna -

Hola Juan Manuel.

Te respondo aunque el resto no creo que entienda tus preguntas y mis respuestas por ahora, ya que no empezamos con el tema de este práctico aún (la clase sobre estos temas será el martes próximo). 

En el ejercicio 11 hay un error. La parte c (3) sustituye a la b (2). Hay que hacer una prueba (o demostración, son sinónimos en este contexto) sin usar tácticas automáticas de Coq y otra usando por ejemplo tauto directamente.

En el ejercicio 12 se aplica lógica clásica; razonar por el tercero excluido.

Saludos, Carlos