madkurt

/dev/kmem

User info:

Registered: Oct 2002
Posts: 45 (0.01 al dì)
Location: Metropolis pt1
Corso: corso fuori
Anno: exp(2)
Time Online: 13:40:58 [...]
Status: Offline

Post actions:

[LPA] problema esercizio (SOLVED)

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!

__________________
Come on everybody! Get toghether!
Try to love one another! Try it now!
TOGHETER WE STAND,
DIVIDED WE FALL!

Last edited by madkurt on 22-07-2008 at 14:22

yeah

.grande:maestro.

User info:

Registered: Nov 2003
Posts: 1644 (0.21 al dì)
Location: Cologno Monzese
Corso: Informatica Magistrale
Anno: II
Time Online: 12 Days, 21:36:41 [...]
Status: Offline

Post actions:

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

/dev/kmem

User info:

Registered: Oct 2002
Posts: 45 (0.01 al dì)
Location: Metropolis pt1
Corso: corso fuori
Anno: exp(2)
Time Online: 13:40:58 [...]
Status: Offline

Post actions:

geniale;)

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

__________________
Come on everybody! Get toghether!
Try to love one another! Try it now!
TOGHETER WE STAND,
DIVIDED WE FALL!

yeah

.grande:maestro.

User info:

Registered: Nov 2003
Posts: 1644 (0.21 al dì)
Location: Cologno Monzese
Corso: Informatica Magistrale
Anno: II
Time Online: 12 Days, 21:36:41 [...]
Status: Offline

Post actions:

Eheh.

Non c'è di che

__________________
?