|
Eugenio86
Utente medio
Regione: Puglia
Prov.: Bari
Città: Bisceglie
|
 Inserito il - 12/06/2010 : 17:42:46
|
Ragazzi ho un dubbio sul principio di risoluzione.
Quando durante il procedimento di risoluzione deduco una nuova clausa applicando l'unificazione, questa si propaga in tutte le altre?
Esempio:
1. { Levriero(L) }
2. { ¬Coniglio(z), PiuVeloce(L,z) }
3. { ¬Levriero(y), Cane(y) }
4. { ¬Cavallo(x), ¬Cane(y), PiuVeloce(x,y) }
5. { ¬PiuVeloce(x,y), ¬PiuVeloce(y,z), PiuVeloce(x,z) }
6. { Cavallo(F) }
7. { Coniglio(R) }
8. { ¬PiuVeloce(F,R) }
----------------------------------------
9. { PiuVeloce(L,R) } z/R (2,7)
...
da questo punto in poi considero l'unificazione z/R su tutte le clause vecchie e nuove? Oppure ad ogni passo considero la z come una variabile ancora unificabile con altri valori?
|
 |
Modificato da - Eugenio86 in Data 12/06/2010 17:43:15
|
|
Risoluzione
