Buenas, estamos trancados con estos dos ejercicios en formas parecidas. Es como que llegamos a un punto en que entramos en loop, en ambos casos nos queda una pata de la derivación que no logramos terminar.
Nos parece que debe ser un tema conceptual que no estamos entendiendo del todo, alguna recomendacion? a alguien mas le pasa algo parecido?
Saludos!
Luego de formalizar los enunciados, la idea es pensar en cada prueba independientemente de Coq. Esto es, pensar una estrategia de prueba que permita demostrar la conclusión a partir de las hipótesis. Sino, es muy fácil perderse al aplicar tácticas de Coq sin una idea clara de los objetivos que se espera alcanzar.
En ambos problemas (11 y 12) se puede usar lógica clásica (en particular el tercero excluido). Por ejemplo, para el problema 12 se puede usar en la prueba el tercero excluido con PR; esto es: elim (classic PR). Asumo que la formalización que hicieron está bien. Para este ejercicio, les doy las fórmulas:
Hypothesis Regla1: PF \/ PA -> PH \/ PR.
Hypothesis Regla2: ~PR \/ PF.
Hypothesis Regla3: PH /\ ~PR -> PA.
Theorem ej12: (~PA /\ PF) -> PR.
...
El martes próximo podemos ver dudas que tengan. Puedo estar de 16:30 a 18hs en el salón habitual (lleven laptop).
De todas maneras, escriban si tienen más dudas o si llegan a cierto punto y a partir de allí se les complica seguir.
Saludos, Carlos
Gracias Carlos, me quedo tranquilo que la traducción estaba bien. Habíamos estado probando con elim (classic PR) pero todavia no logramos cerrar la prueba.
Seguimos probando y cualquier cosa te escribimos para el martes.
Muchas gracias, saludos!
Santiago
Hola.
El martes próximo puedo estar una hora a partir de la hora 17. Si veo que se necesitan más consultas podemos por otra hora o un poco más el día siguiente (miércoles).
Sería bueno saber si han podido avanzar con los ejercicios 11 y 12.
Saludos, Carlos
Hola,
Me serviría mucho si mañana hay clase de consulta para el práctico. También estoy trancada en el ejercicio 11 y 12 en una especie de loop en que siempre termino teniendo que probar PR (en el ejercicio 12) y "salir los domingos" en el ejercicio 11.
Gracias y saludos,
Noelia
Hola.
Ok, nos vemos mañana martes a la hora 17.
Saludos, Carlos
Hola,
Carlos está con un problema de salud. Yo puedo cubrirlo hoy. Les agradezco por favor me confirmen quienes estarían viniendo a la clase de consulta.
Saludos,
Gustavo
Hola.
En esta oportunidad pueden también escribirme a mi correo (cluna@fing.edu.uy) si tienen algún problema puntual con algún ejercicio y es difícil plantearlo al foro del curso. Voy a estar conectado, de a ratos, pero no puedo trasladarme, por eso no puedo estar en la clase de hoy.
Saludos, Carlos
Hola,
Si se hace la clase, yo iría, pero si la clase es solo por una persona y prefieren resolver las consultas por mail, no tengo problema.
Saludos,
Noelia
Hola Noelia,
Hasta ahora solamente vos has confirmado que asistirías a la clase.
Yo voy a estar en el InCo, si te pareec bien, podés pasar por mi oficina y te contesto las dudas. Es la 126.
Saludos,
Gustavo
Estimados,
Finalmente pudimos cerrar las pruebas y no nos quedó ningún ejercicio pendiente, por lo que les confirmo que no vamos a la clase de consulta.
Muchas gracias
Saludos
Santiago
