.dsy:it. (http://www.dsy.it/forum/)
- Logica matematica (http://www.dsy.it/forum/forumdisplay.php?forumid=246)
-- dobbi su fattorizzazione destra (http://www.dsy.it/forum/showthread.php?threadid=31004)

dubbi su fattorizzazione destra

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

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))