 |
Gilbert |
.grande:maestro.
Registered: Oct 2005
Posts: 680 (0.09 al dì)
Location: Milano
Corso: T.I.COM.
Anno: Dott.Mag.!!!!!
Time Online: 7 Days, 10:38:55 [...]
Status: Offline
Edit | Report | IP: Logged |
[LPA] SPASS - mgu e massimali
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.
Last edited by Gilbert on 08-09-2006 at 10:43
|
Gilbert
