Se pide dar una derivacion de
(∀x)f(x, co)='x , (∀x)f(co, x)='x |- (∀y)((∀x)g(x,y)='x → y='co)
No logro hacer bien esa derivacion.. lo que puedo hacer es una derivacion pero usando solo una de las hipotesis, eso esta mal no?
En respuesta a Gabriela Nataly Wynants Lombardini
Re: parcial 2010 ejercicio 3.b
de Matias Rodal Medina -
Las hipotesis de la der tienen q estan incluidas en el conjunto de formulas que tenes disponible para usar, así que si, estaria bien.. por ejemplo si te piden
(∀x)f(x, co)='x , (∀x)f(co, x)='x |- ¬bottom
no va a estar mal la derivacion porque no uses todo. a mi me salio tambien sin una hip. mientras las reglas esten bien usadas esta bien
Saludos
En respuesta a Matias Rodal Medina
Re: parcial 2010 ejercicio 3.b
Ahi va, muchas gracias!
En respuesta a Gabriela Nataly Wynants Lombardini
Re: parcial 2010 ejercicio 3.b
Alguno me puede dar una mano de como hacer esta derivación??
La verdad que no me doy cuenta...
Al principio no me salía porque habia leido mal lo que pedian derivar. Si te paso lo mismo trata de hacerla, si no segui leyendo.
Cuando llegas a que tenes que probar y=c0, esa parte sale con RI3. Tenes que conseguir algo del tipo y=algo y otra cosa del tipo algo'=c0. Trata de interpretar semanticamente que quieren decir las hipotesis que tenes.
A ver si sale ahi, si no te tiro alguna pista mas
En respuesta a Matias Rodal Medina
Re: parcial 2010 ejercicio 3.b
Me decis como lo hiciste? Hace rato estoy pensando y no me sale..
En respuesta a Gabriel Valentin Rodriguez Pena
Re: parcial 2010 ejercicio 3.b
de Matias Rodal Medina -
Ok. De abajo para arriba:
intro del paratodo
intro del implica
RI3 con y=f(c0,y) , f(c0,y)=c0
la der de y=f(c0,y) es: RI2 y Eliminacion del paratodo sustituyendo x por y
la der de f(c0,y)=c0 es una eliminacion del para todo sustituyendo x por c0
Saludos
En respuesta a Matias Rodal Medina
Re: parcial 2010 ejercicio 3.b
Muchas gracias!!
Buenas.. Hasta ahí te seguí, pero como justificás la intro del paratodo?
"y" no tiene que ocurrir libre en las hipótesis sin cancelar que tenés hasta el momento, no? En este caso, debe estar "ligada" a (All x)f(c,x)='x.
Como justifico eso? Debo estar pasando por alto algo muy obvio pero no me doy cuenta..
Muchas Gracias..
en esa hipotesis "y" no ocurre libre, de hecho no ocurre directamente, así que no hay problema
Impecable enconces.. Gracias!