Parciales

Este es el mensaje en cuestión, donde el docente Luis Sierra explica como usar RI4 en yoda:

te cuento de RI4* primero, luego de RI4. para eso, uso un ejemplo que NO tiene porque ser derivable.

en el eva, ingreso (con el lenguaje por defecto) la conclusión

Q(g(a,y),a)

al aplicar la regla RI4* la interfase me pone dos ventanas; una para el esquema de fórmula a usar,
y otro para los términos. siguiendo la nomenclatura de las slides del curso,
lo que hay que colocar en los términos es una lista t0;t1; ... (separada por ;) de términos
eventualmente desconocidos hasta ese momento. en nuestro caso, podemos poner,
por ejemplo, g(x,y);x. en el esquema de fórmula tenemos que
poner la phi original de las slides, la que usa variables zi, aunque en lugar de zi, 
debemos usar $i. por ejemplo, podríamos poner Q(g(a,$0),$1). la aplicación de la regla
genera tres nuevas subpruebas, con futuras conclusiones g(x,y)=y, x=a, Q(g(a,g(x,y)),x).
ahora, un ejemplo para RI4. en el eva, ingreso (con el lenguaje por defecto) la conclusión

g(a,y) = g(g(a,a), x)

al aplicar la regla RI4 la interfase me pone una ventana para los términos. 
hay que colocar un esquema de término como el t original de las slides,
la que usa variables zi, aunque en lugar de zi, debemos usar $i. por ejemplo,
podríamos poner g($0,$1). la aplicación de la regla genera dos nuevas subpruebas, 
con futuras conclusiones a=g(a,a), y=x.

luis