.dsy:it. - dobbi su fattorizzazione destra

.dsy:it.
//www.dsy.it

dobbi su fattorizzazione destra

Posted by dicane on 08-06-2007 10:29

sulle dispense di ghilardi c'e' il seguente esempio (Pag 26):

=> R(x, f(y)), R(y, f(x))

da questa viene dedotta la seguente tramite fattorizzazione destra:

=>R(x, f(x))

Io ho provato ad applicare la regola ma non riesco a capire come possa uscire quel risultato...

Applicando l'unificazione tra le due formule io trovo x -> y e y -> x
Oppure rinominando la x e la y nella seconda (non so se e' necessario rinominare) trovo x -> y1, y->x1

quindi il risultato sarebbe R(y, f(x)) o R(y1, f(x1))
oppure cancellando l'altra premessa R(x, f(y)) o R(x1, f(y1))

Qualcuno puo spiegarmi come va fatto?? GRAZIE