 | |
Il progetto dsy.it è l'unofficial support site dei corsi di laurea del Dipartimento di Scienze dell'Informazione e del Dipartimento di Informatica e Comunicazione della Statale di Milano. E' un servizio degli studenti per gli studenti, curato in modo no-profit da un gruppo di essi. I nostri servizi comprendono aree di discussione per ogni Corso di Laurea, un'area download per lo scambio file, una raccolta di link e un motore di ricerca, il supporto agli studenti lavoratori, il forum hosting per Professori e studenti, i blog, e molto altro...
In questa sezione è indicizzato in textonly il contenuto del nostro forum |
[Logica per app]Traccia B1
Clicca QUI per vedere il messaggio nel forum |
| Logan12584 |
Mi sorge un dubbio malefico...
Con la traccia b1 dobbiamo portare un esercizio con l'uguaglianza e la sovrapposizione o possiamo portare un esercizio con l'ugualgianza ma che si risolve attraverso una risoluzione ( portando quindi 2 esercizi uno senza uguglianza, abbastanza tosto e uno con uguaglianza) ?
p.s.: spero di essermi spiegato dato che sono le 23 e sono 12 ore che studio :| |
| yeah |
Come fai la tua seconda ipotesi? Disabiliti le regole per la sovrapposizione?
Io opto per un problema senza uguaglianza e uno con, ma non ho seguito quest'anno, quindi mi baso su quanto leggo sul suo sito, non so cosa abbia detto a lezione. |
| Logan12584 |
| no perchè il mio problema con l'uguaglianza è talmente facile che si risolve con una res, senza sovrapposizione o altro, per questo chiedevo |
| monik |
Originally posted by Logan12584
no perchè il mio problema con l'uguaglianza è talmente facile che si risolve con una res, senza sovrapposizione o altro, per questo chiedevo
i problemi che ho preso io sono: PUZ012-1+rm_eq_rstfp (senza identità) e PUZ001+1+rm_eq_rstfp (con identità), dalla sezione PUZ. possono andare bene secondo voi? ho dei dubbi perchè quello senza identità mi sembra più facile di quello con identità! e poi è normale che quello con identità non abbia le formule, ma clausole?va bene lo stesso? :? |
| c3ru |
ma bisogna portare due problemi?
se ho fatto la traccia B1 non ne basta portarne uno con identità? |
| Logan12584 |
Originally posted by c3ru
ma bisogna portare due problemi?
se ho fatto la traccia B1 non ne basta portarne uno con identità?
in teoria si, basta che ci sia tutto |
| monik |
Originally posted by c3ru
ma bisogna portare due problemi?
se ho fatto la traccia B1 non ne basta portarne uno con identità?
no, qui dice che bisogna portarne 2: http://homes.dsi.unimi.it/%7Eghilardi/ls/alleg/FAQ.html
Ma io li ho scelti tutti e due nella sezione PUZ, ho sbagliato? li ho segnalati sopra....qualcuno di voi mi sa dire se possono andare bene? nel senso se ho scelto bene quello con identità e quello senza... :( please |
| bluone |
Originally posted by monik
no, qui dice che bisogna portarne 2: http://homes.dsi.unimi.it/%7Eghilardi/ls/alleg/FAQ.html
Ma io li ho scelti tutti e due nella sezione PUZ, ho sbagliato? li ho segnalati sopra....qualcuno di voi mi sa dire se possono andare bene? nel senso se ho scelto bene quello con identità e quello senza... :( please
Su quello senza identità mi sembra sia corretto, su quello con l'identità non sono sicuro l'ho eseguito chiedendo a spass solo il docproof e mi è uscito questo:
Here is a proof with depth 4, length 24 :
2[0:Inp] || -> lives(butler)*.
4[0:Inp] || richer(U,V)+ killed(U,V)* -> .
5[0:Inp] || hates(charles,U)+ hates(agatha,U)* -> .
6[0:Inp] || hates(U,charles)+ hates(U,butler) hates(U,agatha)* -> .
7[0:Inp] || -> hates(agatha,agatha)*.
8[0:Inp] || -> hates(agatha,charles)*.
9[0:Inp] || killed(U,V)+ -> hates(U,V)*.
10[0:Inp] || hates(agatha,U)*+ -> hates(butler,U).
11[0:Inp] lives(U) || -> richer(U,agatha) hates(butler,U)*.
12[0:Inp] || -> killed(charles,agatha) killed(butler,agatha)*.
16[1:Spt:12.0] || -> killed(charles,agatha)*.
17[0:Res:8.0,10.0] || -> hates(butler,charles)*.
18[0:Res:7.0,10.0] || -> hates(butler,agatha)*.
19[1:Res:16.0,9.0] || -> hates(charles,agatha)*.
20[1:Res:19.0,5.0] || hates(agatha,agatha)* -> .
21[1:MRR:20.0,7.0] || -> .
22[1:Spt:21.0,12.0,16.0] || killed(charles,agatha)*+ -> .
23[1:Spt:21.0,12.1] || -> killed(butler,agatha)*.
27[0:Res:17.0,6.0] || hates(butler,butler) hates(butler,agatha)* -> .
29[0:MRR:27.1,18.0] || hates(butler,butler)*+ -> .
30[0:Res:11.2,29.0] lives(butler) || -> richer(butler,agatha)*.
31[0:SSi:30.0,2.0] || -> richer(butler,agatha)*.
32[0:Res:31.0,4.0] || killed(butler,agatha)* -> .
33[1:MRR:32.0,23.0] || -> .
Tu mi sai dire cosa sono SpT e SSi.....
Io per l'identità ero abituato a vedere nei listati la SpR e la SpL oppure EqR ed EqF
Magari mi sbaglio, in effeti anch'io ho dei problemi a trovare un esercizio con l'identità che utilizzi queste regole, perchè di solito tra le MRR e le RES l'esercizio termina sempre senza applicarle....
Qualcuno di buona volontà che ci possa indicare un bel esercizio con l'identità????? |
| monik |
Originally posted by bluone
Su quello senza identità mi sembra sia corretto, su quello con l'identità non sono sicuro l'ho eseguito chiedendo a spass solo il docproof e mi è uscito questo:
Here is a proof with depth 4, length 24 :
2[0:Inp] || -> lives(butler)*.
4[0:Inp] || richer(U,V)+ killed(U,V)* -> .
5[0:Inp] || hates(charles,U)+ hates(agatha,U)* -> .
6[0:Inp] || hates(U,charles)+ hates(U,butler) hates(U,agatha)* -> .
7[0:Inp] || -> hates(agatha,agatha)*.
8[0:Inp] || -> hates(agatha,charles)*.
9[0:Inp] || killed(U,V)+ -> hates(U,V)*.
10[0:Inp] || hates(agatha,U)*+ -> hates(butler,U).
11[0:Inp] lives(U) || -> richer(U,agatha) hates(butler,U)*.
12[0:Inp] || -> killed(charles,agatha) killed(butler,agatha)*.
16[1:Spt:12.0] || -> killed(charles,agatha)*.
17[0:Res:8.0,10.0] || -> hates(butler,charles)*.
18[0:Res:7.0,10.0] || -> hates(butler,agatha)*.
19[1:Res:16.0,9.0] || -> hates(charles,agatha)*.
20[1:Res:19.0,5.0] || hates(agatha,agatha)* -> .
21[1:MRR:20.0,7.0] || -> .
22[1:Spt:21.0,12.0,16.0] || killed(charles,agatha)*+ -> .
23[1:Spt:21.0,12.1] || -> killed(butler,agatha)*.
27[0:Res:17.0,6.0] || hates(butler,butler) hates(butler,agatha)* -> .
29[0:MRR:27.1,18.0] || hates(butler,butler)*+ -> .
30[0:Res:11.2,29.0] lives(butler) || -> richer(butler,agatha)*.
31[0:SSi:30.0,2.0] || -> richer(butler,agatha)*.
32[0:Res:31.0,4.0] || killed(butler,agatha)* -> .
33[1:MRR:32.0,23.0] || -> .
Tu mi sai dire cosa sono SpT e SSi.....
Io per l'identità ero abituato a vedere nei listati la SpR e la SpL oppure EqR ed EqF
Magari mi sbaglio, in effeti anch'io ho dei problemi a trovare un esercizio con l'identità che utilizzi queste regole, perchè di solito tra le MRR e le RES l'esercizio termina sempre senza applicarle....
Qualcuno di buona volontà che ci possa indicare un bel esercizio con l'identità?????
SSi non so cosa sia...ma a me non lo da. Per quanto riguarda SpT dovresti disattivare lo splits!
Setta queste opzioni -DocProof -Sorts=0 -PDer=1 -CNFRenaming -Splits=0 -IEmS=0 -ISoR=0 e dovresti essere a posto... |
| bluone |
Ok con le option che mi hai scritto e che uso anch'io, ma che non avevo attivato nella risolluzione di prima, non compare più la regola degli splits, ma permane il mio dubbio sul fatto che per arrivare alla soluzione non utilizza le regola per l'idemtità. Come puoi vedere dal listato qui sotto utilizza sempre e solo la MRR e la RES.
La SpL o SPr o le altre regole per l'identità non vengono usate. Col problema che ho scelto io è la stessa cosa, perchè esiste l'identità ma poi utilizzando spass la risoluzione si riduce ad MRR e Res sul listato.
Secondo te va bene lo stesso?
Ti metto
2[0:Inp] || -> lives(butler)*.
4[0:Inp] || richer(U,V)+ killed(U,V)* -> .
5[0:Inp] || hates(charles,U)+ hates(agatha,U)* -> .
6[0:Inp] || hates(U,charles)+ hates(U,butler) hates(U,agatha)* -> .
7[0:Inp] || -> hates(agatha,agatha)*.
8[0:Inp] || -> hates(agatha,charles)*.
9[0:Inp] || killed(U,V)+ -> hates(U,V)*.
10[0:Inp] || hates(agatha,U)*+ -> hates(butler,U).
11[0:Inp] || lives(U)+ -> richer(U,agatha) hates(butler,U)*.
12[0:Inp] || -> killed(charles,agatha) killed(butler,agatha)*.
16[0:Res:8.0,10.0] || -> hates(butler,charles)*.
17[0:Res:7.0,10.0] || -> hates(butler,agatha)*.
20[0:Res:2.0,11.0] || -> richer(butler,agatha) hates(butler,butler)*.
23[0:Res:16.0,6.0] || hates(butler,butler) hates(butler,agatha)* -> .
25[0:MRR:23.1,17.0] || hates(butler,butler)* -> .
26[0:MRR:20.1,25.0] || -> richer(butler,agatha)*.
27[0:Res:26.0,4.0] || killed(butler,agatha)* -> .
28[0:MRR:12.1,27.0] || -> killed(charles,agatha)*.
29[0:Res:28.0,9.0] || -> hates(charles,agatha)*.
30[0:Res:29.0,5.0] || hates(agatha,agatha)* -> .
31[0:MRR:30.0,7.0] || -> . |
| monik |
Penso vada bene ugualmente, ma se posso darti un consiglio...non portargli il problema di zia Agatha perchè è stato già fatto a lezione e non vuole che lo si porti anche all'orale!
Il mio problema è che i problemi con l'identità che ho trovato sono messi già sottoforma di clausole, e non sottoforma di formule come ad esempio quello di zia Agatha, e non so se al prof può andare bene ugualmente!!! |
| Nvideo |
Ciao vi propongo il mio dubbio:
la 192 è ottenuta per RES dalle precedenti
102 || bird(U) animal(V) grain(W)* eats(V,U)*+ -> .
186 || -> eats(skc7,skc8)*.
192[0:Res:186.0,102.3] || bird(skc8) animal(skc7)* grain(U)* ->
Non riesco a capire come è accaduto il passaggio della variabile W in U.
Si tratta semplicemente di un uso ottimizzato delle variabili, dato che U non è più necessaria? |
| pumpkin |
| si esatto...anche io sto portando lo stesso problema...me ne sono reso conto dopo qualche passaggio...per spass ci sono variabili diciamo con "maggior priorità" (l'ordine è U, V, W, Z mi pare di aver capito)....quindi una volta che non sono più usate o sono state eliminate da qualche regola di riduzione le riutilizza andandole a sostituire alle altre variabili... |
| Nvideo |
ottimo ottimo.
Almeno se Ghilardi me lo chiede non dico una cappella cosmica!
Secondo te cosa ci chiederà all'orale?
Grazie per la risposta!!! |
|
|
|
|
