[LPA] SPASS - mgu e massimali
Clicca QUI per vedere il messaggio nel forum |
| Gilbert |
Usando spass a volte mi imbatto in cose strane che non riesco a capire, vorrei capire dove sbaglio.
1) Nel calcolo dell'MGU (upg o come volete) tra less(U,V) e less(zero, U)
io farei questi passaggi:
- U = zero / V = U
- U = zero / V = zero
Invece SPASS si ferma al primo, ovvero sostituisce U con zero e V con U. Ma l'algoritmo (vedi dispensa pag. 22) non dice (punto 4) di sostituire, nel caso si incontri una equazione x=t, tutte le occorrenze di x con t?
Possibile motivo: t non deve essere una variabile, ma una variabile in una funzione. In questo caso U non è in una funzione quindi non lo sostituisce.
2) Mi trovo che a volte SPASS effettua risoluzioni tra due clausole usando un letterale massimale ed uno no.
Es.: Risoluzione tra
=> less(b,c)*
e
less(U,V) => equal(divide(U,V), zero)**
viene fatta tra less(b,c) e less(U,V).
E' chiaro che non sarebbe stato possibile farla con il secondo letterale della seconda clausola, ma non si doveva evitare di fare la risoluzione del tutto?
La dispensa (pag. 42) dice: "Nei dimostratori automatici come SPASS, i letterali massimali vengono memorizzati mediante un asterisco: in tal modo, vengono prese in considerazione solo le inferenze che coinvolgono letterali asteriscati."
Vuol dire che ne basta uno o che devono essere entrambi asteriscati?
Possibile motivo: basta che l'inferenza coinvolga un solo letterale asteriscato.
3) Usando un lpo e come precedenza divide>zero>c>a e calcolando i massimali, mi trovo questa cosa:
divide(a,c) = zero**
Per esserci il doppio asterisco è necessario che divide(a,c) >lpo zero
Per LPO1 dovrei avere che a>=zero oppure c>=zero ma nessuna di queste condizioni è vera.
Oppure devo considerare zero come una funzione di arietà zero?
In tal caso per LPO2 ho che divide>zero e a>(nulla) e c>(nulla).
Però bisogna mettersi d'accordo. Perchè in LPO1 t è un termine (quindi può essere anche una costante e quindi una funzione di arietà 0).
Quando sono di fronte ad una costante la devo vedere come termine o come funzione di arietà 0? (che poi è la stessa cosa, ma per LPO pare di no...)
Possibile motivo: le costanti vanno viste sempre come funzioni di arietà 0 in LPO. |
| Gilbert |
| Nessuno sta preparando logica e vuole darmi una mano? |
| Barone |
| Alla seconda domanda risponderei che probabilmente avviene una post ordered check..cioè dopo aver applicato alla clausola il mgu scopre che in realtà less(U,V) è il letterale massimale e quindi utilizza quello in luogo di quello precedentemente asteriscato..spero di averci preso. |
| Gilbert |
Non può essere così perchè il letterale asteriscato nella seconda clausola è positivo, così come quelo nella prima. In tal caso non è possibile fare la risoluzione (ce ne vuole uno positivo ed uno negativo).
Per quanto riguarda la prima domanda, sicuramente è dovuto al fatto che dato che i due letterali fanno parte di due clausole tra le quali viene effettuata risoluzione, è necessario rinominare le variabili in comune (infatti devono essere disgiunte). Per cui, la "U" del secondo letterale non è la stessa "U" del primo.. |
|
|
|
