problema con MRR
Clicca QUI per vedere il messaggio nel forum |
| rasta84 |
Non ho mai visto l'applicazione della regola MRR, quindi ho difficoltà nel fare a mano questa inferenza:
14[0:MRR:7.0,1.0] || -> L(b)*.
dove le clausole 7 e 1 sono le seguenti:
7[0:Inp] || T(a) -> L(b)*.
1[0:Inp] || -> T(a)*.
Qualcuno riesce a spiegarmi i passaggi, x favore? |
| rasta84 |
proprio nessuno riesce ad aiutarmi con la MRR?
Vi spiego un po' meglio il problema..
Da quello che ho capito dalla dispensa (guardate l'allegato) questa regola di riduzione cancella una delle due premesse e ne crea una nuova più semplice, solo se vengono rispettate le tre condizioni.
Quello che non capisco è perchè nella dimostrazione del mio problema, Spass sembra fregarsene di queste condizioni. Tra l'altro in alcuni casi trova un matcher anche se l'algoritmo di mathing dovrebbe restituire FAIL per i letterali che vengono scelti..
Per esempio:
17[0:MRR:9.0,1.0] || -> T(a)* T(b).
dove le clausole 9 e 1 sono:
9[0:Inp] || L(b)* -> T(b) T(a).
1[0:Inp] || -> T(U) L(U)*.
matcha il letterale 0 della clausola 9 (L(b)) con il letterale 0 della clausola 1 (T(U)). Il matching non dovrebbe fallire visto che i simboli in radice per i due letterali sono diversi? |
| Logan12584 |
a me non è mai capitato che facessi questo tipo di risoluzione... hai provato a disabilitare il renaming ?
-CNFRenaming=0
a quest'ora dico puttanate ti avverto, ma tentare non nuoce |
| yeah |
| Sulla MRR non mi pronuncio perché devo ancora rivederla (insieme alle altre). In questi giorni l'unificazione tra letterali apparentemente "errati" purtroppo è capitata anche a me e non sono ancora riuscito a capire cosa significhi. |
| rasta84 |
Infatti, mi è capitato una scelta di letterali sbagliati anche per la resolution e non riesco a spiegarmi il motivo..
Disattivando la MRR funziona tutto bene, solo che ho paura che al prof non vada bene... |
| Logan12584 |
si sa nulla su questo problema?
Neanceh a farlo a posta ho avuto lo stesso prob su un eserc con identità, la cosa bella è che anche la sovrapposizione dx sembra sbagliata perchè da una parte c'è l'uguaglianza, mentre nell altra clausola non c'è una identità ma una funzione generica... |
| yeah |
| Prova disattivando la saturazione dell'input, con -SatInput=0 e dimmi se succede ancora |
| Logan12584 |
Originally posted by yeah
Prova disattivando la saturazione dell'input, con -SatInput=0 e dimmi se succede ancora
non cambia nulla |
| mattcobain |
| Ragazzi ma come si disattiva la MRR? |
| yeah |
| -RMRR=0 o qualcosa del genere, guarda sulle opzioni di SPASS ;) |
|
|
|
