CFPTT: [Practico 1] Ejercicio 9

No logro que me salga el ejercicio 9, ya intente todo lo que se me ocurrio. Alguna recomendacion que me pueda ayudar?

No logro visualizar como lo demostraria sin tirar reglas una atras de la otra. Se que dijeron que no hagamos esto pero...

Variable NM:Prop. (* Base de datos Normalizada*)

Variable RED:Prop. (* Presenta Redundancia de Informacion*)

Variable CONS:Prop. (* Es Consistente*)

Variable UTIL:Prop. (* Es Util*)

Hypothesis H1 : ~NM \/ ~RED.

Hypothesis H2 : CONS \/ ~UTIL.

Theorem ej9 : NM /\ UTIL -> CONS /\ ~RED.

Esta bien planteado el problema por lo menos?

Saludos

Re: [Practico 1] Ejercicio 9

de Carlos Luna - miércoles, 17 de agosto de 2022, 10:39

Hola Alejandro.

Intenté responder más temprano pero el EVA tenía problemas.

La formalización que hiciste en el problema 9 es correcta.

Para probar el teorema, fijate que vas a tener las hipótesis H1, H2 y las dos que generes del goal prinicipal (para NM y UTIL). En concreto, el objetivo es probar CONS y ~RED (luego de que hagas split en el /\).

Para CONS, fijate que H2 te da información relevante (tendrías que hacer elim H2); un caso sale trivialmente y en el otro vas a tener ~UTIL para probar CONS, pero también tenés UTIL (acá podés usar por ejemplo absurd UTIL y sale fácil).
Para ~RED fijate que H1 es la que ahora te da información relevante (tendrías que hacer elim H1); en un caso fijate que vas a tener NM y ~NM (podés usar, por ejemplo, absurd con MM) y el otro es trivial.

Bueno, espero que esto te ayude y sino volvé a escribir.

Saludos, Carlos

Re: [Practico 1] Ejercicio 9

de Alejandro Sebastian Flocken Rodriguez - miércoles, 17 de agosto de 2022, 11:43

Ok, gracias ya me salio, aunque me llevo mas pasos me parece que los que pusiste.
Una duda:

Cuando yo estoy en esta situacion:

NM, RED, CONS, UTIL : Prop
H1 : ~ NM \/ ~ RED
H2 : CONS \/ ~ UTIL
H : NM /\ UTIL
H0 : ~ UTIL
______________________________________(1/2)
CONS
______________________________________(2/2)
~ RED

Y me decis que aplique absurd(UTIL). Como se lee o razona el absurdo?
Porque cuando hago el elim(H2), mi razonamiento es que quiero eliminar esa Hipotesis entonces tengo que demopstrar que tanto CONS -> CONS y ~UTIL -> CONS se cuimplen porque es equivalente. Pero el absurdo como es?

Porque acto siguiente te queda asi:

3 goals

NM, RED, CONS, UTIL : Prop

H1 : ~ NM \/ ~ RED

H2 : CONS \/ ~ UTIL

H : NM /\ UTIL

H0 : ~ UTIL

______________________________________(1/3)

~ UTIL

______________________________________(2/3)

UTIL

______________________________________(3/3)

~ RED

Saludos.

Re: [Practico 1] Ejercicio 9

de Carlos Luna - miércoles, 17 de agosto de 2022, 12:57

Hola.

En lo primero que ponés fijate que en H tenés UTIL (al eliminar el /\) y ~UTIL (H0). De ambos surge una contradicción; desde el punto de vista lógico, de False se deduce cualquier cosa.

Al hacer absurd(UTIL) se pide probar UTIL y ~UTIL para probar el goal.

Otra opción seía elim(H0 H_UTIL), donde H_UTIL sería una prueba de UTIL (que surge al desarmar H). Notar que este elim se aplica a False ya que (H0 H_UTIL) es False (recordar que ~X es X->False).

Espero esto aclare tus dudas.

Saludos, Carlos