dobbi su fattorizzazione destra
Clicca QUI per vedere il messaggio nel forum |
| dicane |
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 |
| dicane |
ok ci sono arrivato :P bisogna applicare la regola SUB quando si ha una cosa del tipo x=?y, y=?x quindi l'unificazione diventa
x=?y, y=?y
cancello la seconda e resta
x=?y
applico la sostituzione x->y e ottengo
R(y, f(y)) |
|
|
|
