dicane

.illuminato.

User info:

Registered: Oct 2005
Posts: 218 (0.03 al dì)
Location: Milano
Corso: Informatica
Anno: non ricordo :)
Time Online: 4 Days, 8:12:04: [...]
Status: Offline

Post actions:

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

Last edited by dicane on 08-06-2007 at 13:35

dicane

.illuminato.

User info:

Registered: Oct 2005
Posts: 218 (0.03 al dì)
Location: Milano
Corso: Informatica
Anno: non ricordo :)
Time Online: 4 Days, 8:12:04: [...]
Status: Offline

Post actions:

ok ci sono arrivato 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))