[LPA] problema esercizio (HELP)
Clicca QUI per vedere il messaggio nel forum |
| madkurt |
Ciao a tutti,
ho formalizzato il problema PUZ-31 e sto studiandone la dimostrazione data da spass impostato con RPOS (LPO).
Accade ripetutamente che effettui la risoluzione tra il letterale destro asteriscato (strettamente massimale) di una clausola; ed il letterale sinistro NON asteriscato di un'altra clausola -che ha altri letterali asteriscati (massimali)- ..
Secondo quanto dice il Prof, la risoluzione ordinata è possibile SOLO tra letterali massimali, in cui quello destro deve essere per forza strettamente massimale, mentre quello sinistro basta che sia massimale.
Nel mio caso tuttavia quello sinistro non è affatto massimale; ho controllato con la definizione ricorsiva di LPO ed è così: quel letterale NON è massimale perché è maggiorato da un'altro -mangia(U,W)-, infatti non è asteriscato.
Eppure SPASS (sia la 3 che la 2.2) lo utilizza lo stesso nella risoluzione.
Ecco un esempio:
20[0:Inp] || lumaca(U) uccello(V) -> piu_piccolo(U,V)*.
26[0:Inp] || animale(U) pianta(V) animale(W) pianta(X) piu_piccolo(W,U)+ mangia(W,X)* -> mangia(U,V)* mangia(U,W)*.
60[0:Res:20.2,26.4] || lumaca(U) uccello(V) animale(V) pianta(W) animale(U) pianta(X) mangia(U,X)* -> mangia(V,W)* mangia(V,U)*.
L'ordine è questo:
mangia > animale > piu_piccolo > uccello > bruco > volpe > pianta > grano > lumaca > lupo
qualcuno ha una spiegazione?
Grazie in anticipo..
Marco
PS
La soluzione, come scritto più sotto, è molto banale:
il letterale piu_piccolo è segnato con la crocetta, quindi utilizzando la risoluzione con il meccanismo di selezione, spass non solo può utilizzarlo, ma è Obbligato ad utilizzarlo! :) |
| yeah |
Se ben ricordo la crocettatura "ha priorità" sull'asterisco.
E contando le clausole da 0, in 26 usa il letterale crocettato.
[edit]
Puoi disattivare la crocettatura con -Select=0, mi pare. Comunque dai un occhio anche alla dispensa che spiega il meccanismo e l'opzione giusta, perché se porti l'esercizio all'esame può essere che te la chieda :) |
| madkurt |
:D ci ero appena arrivato e stavo per postare un reply ma mi hai anticipato:)
Ieri sera tardi si vede che avevo la testa un po' fusa..
Ad ogni modo è esattamente come dici tu, grazie;) |
| yeah |
Eheh.
Non c'è di che :) |
|
|
|
